*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Makarius <makarius at sketis.net>*Date*: Tue, 12 Nov 2013 17:00:00 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1384271334.2456.34.camel@kirk>*References*: <CANofLeJJ8O2Y2ktXUER1AsH1F4CQsBB21PPbLMVVQa-UfwjgoQ@mail.gmail.com> <353FF788-2AA0-4188-8AAD-28E803A1F647@gmail.com> <CANofLeLVT7QWSUE4HhNy+kq9UuCe4J7gsXVEzma0x_SO5C03wQ@mail.gmail.com> <26755B7F-E696-4A5D-9BE7-9BCFA0FF85B8@gmail.com> <alpine.LNX.2.00.1311111227510.20958@macbroy21.informatik.tu-muenchen.de> <5280E51C.3010703@inf.ethz.ch> <alpine.LNX.2.00.1311111531350.10735@macbroy21.informatik.tu-muenchen.de> <52822B89.40809@in.tum.de> <52822EAB.10505@in.tum.de> <5282348B.8040008@in.tum.de> <528236EB.6050305@in.tum.de> <1384267524.2456.10.camel@kirk> <52824133.5020803@in.tum.de> <1384268947.2456.15.camel@kirk> <alpine.LNX.2.00.1311121619490.24742@macbroy21.informatik.tu-muenchen.de> <52824A76.5090601@in.tum.de> <1384271334.2456.34.camel@kirk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 composemethod (which is configurable and more extentensive) by a hard-codedlist which contains, for example ☭ and ¹, but not the ones you mention,which is unfortunate. This can be overwritten (exportGTK_IM_MODULE="xim" ), but that had other side-effects which I don’trecall at the moment.

\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 Isabelle2013-1).

(The IBus guy did not understand the source of the problem.)

Makarius

**References**:**[isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Makarius

**Re: [isabelle] sledgehammer in RC4***From:*Andreas Lochbihler

**[isabelle] Remaining reasons for Proof General***From:*Makarius

**Re: [isabelle] Remaining reasons for Proof General***From:*Manuel Eberl

**Re: [isabelle] Remaining reasons for Proof General***From:*René Neumann

**Re: [isabelle] Remaining reasons for Proof General***From:*René Neumann

**Re: [isabelle] Remaining reasons for Proof General***From:*Manuel Eberl

**Re: [isabelle] Remaining reasons for Proof General***From:*Joachim Breitner

**Re: [isabelle] Remaining reasons for Proof General***From:*Manuel Eberl

**Re: [isabelle] Remaining reasons for Proof General***From:*Joachim Breitner

**Re: [isabelle] Remaining reasons for Proof General***From:*Makarius

**Re: [isabelle] Remaining reasons for Proof General***From:*René Neumann

**Re: [isabelle] Remaining reasons for Proof General***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Remaining reasons for Proof General
- Next by Date: Re: [isabelle] Remaining reasons for Proof General
- Previous by Thread: Re: [isabelle] Remaining reasons for Proof General
- Next by Thread: Re: [isabelle] Remaining reasons for Proof General
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list