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
 undo-undo.
jEdit:

A -edit-> B -edit-> C -undo-> B -edit-> D -undo-> B (*) -undo-> A
(*) no way to get back to C from here

emacs:

A -edit-> B -edit-> C -undo-> B -edit-> D -undo-> B -undo-> C -undo-> B -undo-> ...

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,
    trackers etc.

  * participate in other PIDE implementations, e.g. Isabelle/Eclipse.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.