Re: [isabelle] Emacs hurts

Am 02.09.2012 14:37, schrieb Rafal Kolanski:
> On 30/08/12 21:24, René Neumann wrote:
>> Am 29.08.2012 20:49, schrieb Christoph LANGE:
>>> I won't subscribe to this list now, so let me mention my two cents here:
>>>  Emacs with Emacs keybindings hurts.  Emacs as an operating system is
>>> great.  I'm using it with vi keybindings.  Not the outdated Viper that
>>> some of you may have heard of, but the vim-like evil
>>> ( 
>> Thanks for this pointer! How did you manage to make the token shortcuts
>> work again in evil (i.e. that --> inserts \<longrightarrow>, !! inserts
>> \<And> etc.)? This seems not to work out of the box.
> I have also embraced evil. In my experience, token shortcuts work after
> you enter insert mode, toggle them off and then on again. They then work
> fine until you restart proof general. I bound a key combo to be able to
> toggle unicode tokens:
> (global-set-key [(control f12)] 'unicode-tokens-mode)

I found a solution that does not require pressing a certain key
combination twice, but does so automatically:

; make unicode-tokens work
(eval-after-load "isar" '(progn
                           (unicode-tokens-use-shortcuts 0)
                           (unicode-tokens-use-shortcuts 1)))

- 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

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