Opened 15 years ago
Closed 15 years ago
#293 closed defect (fixed)
Synchronisation losses with undo-on-edit
| Reported by: | Alexander Krauss | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.1 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | krauss@… |
Description
The following behaviour makes the setting "PG -> Quick Options -> Read only -> Undo on Edit" quite unusable for me.
Steps to reproduce (with Isabelle):
- open some Isabelle theory, eg HOL/Library/Multiset.thy
- go to position (99,0) and do C-c C-RET
- go back to (95,0) and quickly press SPACE twice
(notice that one of the spaces is swallowed, and only one appears in the buffer)
The highlighted region is correct but the prover seems to be somewhere else:
- press C-c C-n
* Illegal application of command "lemma" (line 94 of "/home/krauss/isabelle2009/Isabelle/src/HOL/Library/Multiset.thy") in proof mode * At command "lemma" (line 94 of "/home/krauss/isabelle2009/Isabelle/src/HOL/Library/Multiset.thy").
It may take a few attempts to reproduce this (keypresses must be fast enough). My guess it that some race condition makes the undo happen twice on the prover side...
Using CVS as of 2009-10-02 00:43, GNU Emacs 23.1.1 and Isabelle 2009.
Change History (3)
comment:1 Changed 15 years ago by
| Status: | new → accepted |
|---|
comment:2 Changed 15 years ago by
If a real fix is too complicated, this seems like a good workaround, and I wasn't able to produce any futher sync losses.
The keypresses are still swallowed, which may become a bit annoying. Also, undo-on-edit now fails if the prover is really busy... But it is certainly more usable now.
comment:3 Changed 15 years ago by
| Milestone: | PG-Emacs-4.0 → PG-Emacs-4.1 |
|---|---|
| Resolution: | → fixed |
| Status: | accepted → closed |
Thanks for follow-up. Assuming you only lose key-presses in the case that the prover is busy? I don't think there should be any lost keys otherwise.
I think the error-if-busy is a reasonable approximation for now. It might be more desirable to automatically interrupt and then undo, but the process control is a bit coarse for that and there are anyway problems with interrupt handling (both in Isabelle and PG) that mean it is difficult to strongly rely on interrupts behind the scenes.
If you know the prover's busy you can hit C-c C-c before typing (probably need Follow Mode -> Don't Move for this to make sense).
Thanks for the report Alex. I haven't investigated yet but suspect you're right about a race condition here, perhaps a simple check that the prover is not busy before sending the undo will fix that (committed but not tested).