[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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
> window.

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 
jEdit features.


 	Makarius