Re: [isabelle] isabelle/jedit



Dear Makarius,

you wrote:

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

Genuine interaction in interactive theorem proving is to be able to
concentrate on the course of the proof without more than needed
distraction of technicalities. I think menus could help this, you say
they wouldn't, and they do not fit the picture. What other
possibilites does jEdit have you refer to?

- Gergely





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