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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
