*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 12 Nov 2013 16:36:44 +0100*In-reply-to*: <1384270209.2456.28.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> <alpine.LNX.2.00.1311121601310.24742@macbroy21.informatik.tu-muenchen.de> <52824586.8060409@gmail.com> <1384270209.2456.28.camel@kirk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

Using a compose key is definitely a good way to just ignore jEdit's completion. I have a customised .XCompose file that allows me to write ∀, ∃, ∈, ⟹, ⊆ and so on using the Compose key; this solution has the advantage that it also works the same way outside of jEdit. I only just realised that I could simply use my Compose key to solve the whole Unicode token issue for me, maybe I should give jEdit another try. On 12/11/13 16:30, Joachim Breitner wrote: > Hi, > > Am Dienstag, den 12.11.2013, 16:13 +0100 schrieb bnord: >> I find the "not" case still unpleasant. >> - I can't use "~<TAB>" because it's a composing key so I have to type >> "~<space>C-b<TAB>" > > do you really mean “composing”, in the sense of the Compose key, or > rather “dead” key? > > For a dead key i would expect that <~><space> will print "~", not "~ " – > why do you need Ctrl-B? What OS by the way? > > I have disabled dead keys and use the Compose Key > (https://en.wikipedia.org/wiki/Compose_key) so that <Compose><~><n> > yiels ñ. But that might not be an option if you have to enter a lot of > accents. In that case, you might want to customize jEdit, as suggested > by René¹². > > Greetings, > Joachim > > > ¹ Yes, that is <R><e><n><Compose><´><e>. > ² No, ¹ is not <Compose><^><1>, although that works as well, but > <AltGr><1> > ³ My <Compose> key is <Print>, which Thinkpads have for some reason > between the right AltGr and String. I enable that with > keycode 107 = Multi_key > in my ~/.Xmodmap. > >

**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:*Makarius

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

**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