Re: [isabelle] Remaining reasons for Proof General



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





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