Opened 15 years ago
Closed 14 years ago
#287 closed defect (fixed)
Script management flaws
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.0 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | krauss@… |
Description
Some of the script management code has been generalised and (for Isabelle) linear_undo added. This is not quite perfect yet: it is possible to lose sync (Isabelle) and (Coq) undo behaviour is not right.
Leaving this as a note that this is known (applies to CVS head only; no devel release until this is fixed).
Change History (7)
comment:1 Changed 15 years ago by
comment:2 Changed 15 years ago by
| Cc: | krauss@… added |
|---|
I am still experiencing frequent synchronization loss with current CVS (2009-09-27 20:14) and Isabelle 2009, but I havn't been able to nail this down to a reproducible situation. I'll keep trying.
comment:3 Changed 15 years ago by
| Status: | new → accepted |
|---|
Some changes a couple of days ago should fix script management for Coq now (and perhaps mystery Isabelle failures too?)
comment:4 Changed 15 years ago by
The mystery Isabelle failures are probably unrelated, and I opened a separate ticket (#293).
comment:5 Changed 15 years ago by
Unfortunately (despite dev releases), there are still some script management flaws with Coq. In particular, undoing comments sometimes goes wrong (some state is not being cleared which results in wrong data being stored in some regions in the buffer). This is urgent to fix, but may take until early Nov due to finish because of other commitments.
comment:6 Changed 14 years ago by
A synchronization bug has been fixed in today's CVS which resolves a problem with interrupts that do not cause error messages from the prover. This fixes some occasional sync problems seen with Isabelle.
comment:7 Changed 14 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | accepted → closed |
Fixed a bug in Coq synchronization: proof-shell-restart was not resetting state counters properly. Closing since I think this was the bug mentioned above.
Isabelle script management should now be working.