Re: [isabelle] jEdit problems



On Fri, 26 Jun 2015, Jason Dagit wrote:

Second, I use OS X to remap my keyboard to the dvorak layout, but when I use a modifier key such as control jEdit interprets my keypress incorrectly. I can even see this happening from the keyboard test utility under the troubleshooting menu. This makes it impossible for me to use certain shortcuts or to even use certain keys. This looks similar to my problem: https://bugs.openjdk.java.net/browse/JDK-8028617

This sounds like a generic Java or jEdit problem. You can try plain jEdit from http://www.jedit.org to see if it is the same. Depending on that, we can continue the discussion here or on the jedit tracker http://sourceforge.net/p/jedit/_list/tickets?source=navbar


Fourth, at this point I wanted to go back to using emacs so that at least the first two issues would go away. The official tutorial, dated May of this year, even has this to say: "The recommended interface for Isabelle/Isar is the (X)Emacs-based Proof General [1, 2]."

That is probably the "tutorial" entry in the Documentation collection, but that is fairly outdated. The "prog-prove" tutorial is more up-to-date, although its Isabelle/jEdit screenshot is a bit old.

We have so many manuals from such a long time, that there are many layers of historic sediments. After some time, you should develop a sense which sources of information help in which situation. The "Reference Manuals" section is updated more often, but that is not a tutorial.


But when I tried to connect Proof General to Isabelle, I discovered that it never connects because tty support was removed! So is Proof General still the recommended interface as the tutorial says?

The NEWS file for each Isabelle release is the most up-to-date piece of information. For Isabelle2015 it says:

* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.


	Makarius





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