Re: [isabelle] isabelle/jedit
> 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
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and