*To*: René Neumann <rene.neumann at in.tum.de>*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 12 Nov 2013 15:10:51 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5282348B.8040008@in.tum.de>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

I must admit I did not know about this option before; it must be rather new. However, the behaviour is… odd. It seems to complete as soon as there is only one alternative left, i.e. "\alp" is turned into "α". "\ta" is turne into "τ". When one types "\alpha", one gets "αha", when one types "\tau", one gets "τu". So basically, if one wants to use this feature, one has to remember what part of the abbreviation will lead to there being only one possibly completion. That is not exactly what I had in mind. (On a related note, I also found that jEdit was quite slow; it takes over a minute to start up on my laptop; Proof General is /much/ faster.) On 12/11/13 15:00, René Neumann wrote: > Am 12.11.2013 14:35, schrieb René Neumann: >> Am 12.11.2013 14:22, schrieb Manuel Eberl: >>> 2. Unicode Tokens >>> In Proof General, I type "ALL" and I get a "∀". In jEdit, I type "all", >>> I get an annoying popup and have to confirm my choice with a key press. >>> I have tried to get used to this, but I cannot, even after setting the >>> popup delay to 0 and adding Space and Tab as keys for confirming the >>> currently selected symbol. This is particularly tedious if one types a >>> sequence of symbols. In a way, I feel that users who /know/ their >>> unicode token names by heart are slowed down by unnecessary GUI (the >>> popup). I'd like to be able to switch it off and fall back to a Proof >>> General-like mechanism where I can type "ALL", "==>" and "\<alpha>" and >>> they are immediately converted to the corresponding Unicode token. >> This is what I meant in my email with this blurb about 'unicode'. > Plugin Options -> Isabelle -> General -> Completion Immediate > > Note to self: RTFM before complaining :) > > - René > >

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

**Re: [isabelle] Remaining reasons for Proof General***From:*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

- 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