Re: [isabelle] isabelle/jedit

On Wed, 8 Aug 2012, Gergely Buday wrote:

4.3 Where have all the menus gone?

In Proof General many settings of Isabelle and diagnostic commands could be con gured and started via menus. This is currently not supported in Isabelle/jEdit.

Is there any technical reason for this?

There are conceptual reasons for that. Isabelle/jEdit is not just another clone of Proof General, but based on a timeless and stateless model of continous document processing. This makes it a bit challenging to implement, but I've found 5 years ago that it was high time for the ITP community to move on towards genuine interaction, not just tty command loops.

The model underlying Isabelle/jEdit is still awaiting to be augmented by diagnostic commands as first-class concept. Moreover, I need to add stateless management of options for particular situations.

Menus are just a very superficial thing. Emacs has little other GUI elements than menus, so we used them 15 years ago. jEdit has more possibilities to be put into proper use eventually. So don't wait for an imitation of Proof General Emacs on the jEdit platform. It has quite different side conditions.


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