Re: [isabelle] Remaining reasons for Proof General



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é


-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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