Re: [isabelle] Number of undos
On Tue, 30 Sep 2014, bnord wrote:
Am 30.09.14 um 15:58 schrieb Makarius:
Using Emacs myself over 15 years, I never understood its way of undo or
A -edit-> B -edit-> C -undo-> B -edit-> D -undo-> B (*) -undo-> A
(*) no way to get back to C from here
A -edit-> B -edit-> C -undo-> B -edit-> D -undo-> B -undo-> C -undo-> B
There is an edit stack with an undo pointer, each edit command sets the undo
pointer to the latest element except the undo command which is an edit
command that decrements the undo pointer and reverts the command pointed to
by the undo pointer.
I still don't quite understand the point. Is this now something for the
mailing list of jEdit or Emacs?
Isabelle/jEdit is the second major prover front-end, after Proof General
Emacs, where I was also involved. The editor substrate at the bottom is
given as-is. It has strengths and weaknesses. As an editor I've found
jEdit more onvincing than Emacs, which is why I started this insane PIDE
project, but PIDE is actually independent of editors.
There are two main routes to go from here:
* participate in improvements of jEdit on the jEdit mailing lists,
* participate in other PIDE implementations, e.g. Isabelle/Eclipse.
This archive was generated by a fusion of
Pipermail (Mailman edition) and