Re: [isabelle] Remaining reasons for Proof General

On Tue, 12 Nov 2013, Joachim Breitner wrote:

Am Dienstag, den 12.11.2013, 16:34 +0100 schrieb René Neumann:
As a matter of fact: The Linux' XCompose input method [1] works fairly
well with Isabelle/jEdit. For example, I use my right windows key as
compose key, allowing me to use Compose + / + \ to enter ∧ in any text.
Same for Compose + g + a for α ... and many more.

additional fact: gtk (or GNOME?) disables the usual X11 provided compose method (which is configurable and more extentensive) by a hard-coded list which contains, for example ☭ and ¹, but not the ones you mention, which is unfortunate. This can be overwritten (export GTK_IM_MODULE="xim" ), but that had other side-effects which I don’t recall at the moment.

Here is a probably related note from the last section of the Isabelle/jEdit manual:

  \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
  tend to disrupt key event handling of Java/AWT/Swing.

  \textbf{Workaround:} Do not use input methods, reset the environment
  variable @{verbatim XMODIFIERS} within Isabelle settings (default in

It has required almost 1 year until I managed to reproduce this myself and to find an entry on the IBus tracker, which is still pending, I think.
(The IBus guy did not understand the source of the problem.)

So Linux input methods can be as hostile to Java as window managers. To me that "platform" has become more and more like a freak show.

People who do have the ambition to iron out such snags, are especially welcome to provide further hints to the jEdit guys at

My impression is that the quality and coverage is approx. 90% Windows, 9% Mac OS X, 1% Linux. The little remains of the latter are then potentially destroyed by Linux packagers (but Isabelle/jEdit does not depend on that).


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