[isabelle-dev] jedit

[Makarius]

On Tue, 15 May 2012, Lawrence Paulson wrote:

> I am teaching an Isabelle course right now, and I constantly refer 
> students to various capabilities offered in Proof General's menus. I've 
> never understood how jEdit can do the amazing things it does and yet not 
> offer something as simple as menus.

> Menus should be quite easy to implement.

The menus alone are not so difficult.  One merely needs to spend a little 
time to look closely how jEdit plugins usually do it, and then imitate 
that -- not the old Emacs way, but the jEdit way.

Conceptually, there is a deeper reason why such things outside the main 
editor buffer are not yet supported: the document model is based on 
explicit edits and corresponding changes of the semantic content.  There 
is simply no support yet for diagnostic functions over existing document 
content.  One needs to simulate that by editing the query functions into 
the text, presently by manual editing.  Moreover, many of the PG menu 
operations are actually changing global state variables in the prover 
process, which is incompatible with the asynchronous editor model.

Some of this is explained in the following recent paper on 
"READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking" 
http://www4.in.tum.de/~wenzelm/papers/async-repl.pdf


> Also nice would be palettes of mathematical symbols, although at least 
> Mac users can instead rely on a system-wide Unicode character entry 
> menu.

That's one of the many small convenience that can be imagined.  If someone 
shows me a nice little solution to the problem, I can integrate it. 
(Hopefully not depending on huge useless Java frameworks in the 
background.)

Concerning the generic input method problem, I've learned an interesting 
variant in the Isabelle course yesterday: ASCII tilde is quite hard to 
type on some keyboard variants on Windows -- it was an Arabic keyboard 
with French mapping from French Windows.  Another interesting variant was 
the Asian MacBook with French layout, but I think it worked better. In 
fact, the tilde (and some other ASCII keys) are already known to be 
difficult to produce on Mac OS with German layout.


 	Makarius