[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jun 27 13:51:39 CEST 2014
On Fri, 27 Jun 2014, Peter Lammich wrote:
> * Isabelle/jEdit does not support highlighting of paranthesis in the
> output window (it does work in PG!). This is an essential feature to
> read bigger goal states.
> Moreover, the output buffer does not support middle-mouse-button
> copy-and-paste on my ubuntu-box, while it perfectly works in the editor
PG uses Emacs with its "everything is a buffer model"; Isabelle/jEdit uses
jEdit + Java/AWT/Swing, with slightly different side-conditions. Both have
sometimes advantages, and sometimes disadvantages.
The middle-mouse-button is an ancient X11 idiom that no other platform
knows, and Swing does not support it. The jEdit guys have retrofitted
that ocasionally useful idiom to the standard jEdit text area, but it is
absent in regular Swing GUI components.
You get other benefits from the more "standard" and less Unix/X11-centric
approach in jEdit; it just needs more practice to discover the wealth
More information about the isabelle-dev