Re: [isabelle] Emacs hurts



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
>> (http://gitorious.org/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)

So, open a .thy file, enter insert mode, hit ctrl-F12 ctrl-F12, type
\lambda and you get λ. Same for --> , \forall etc.

Here are some other helpful settings to act more vim-like, and an
example how to do something like :nmap Y y$

(require 'evil)
(evil-mode 1)

(define-key evil-motion-state-map (kbd "<down>") 'evil-next-line)
(define-key evil-motion-state-map (kbd "<up>") 'evil-previous-line)
(define-key evil-motion-state-map (kbd "<left>") 'evil-backward-char)
(define-key evil-motion-state-map (kbd "<right>") 'evil-forward-char)
(define-key evil-normal-state-map (kbd "<insert>") 'evil-insert)
(define-key evil-insert-state-map (kbd "<insert>") 'evil-replace-state)
(define-key evil-replace-state-map (kbd "<insert>") 'evil-insert-state)
(define-key evil-normal-state-map (kbd "<delete>") 'evil-delete-char)

(evil-define-operator evil-yank-line-end (beg end type register)
  "Yank to end of line."
  :motion evil-end-of-line
  (interactive "<R><x>")
  (evil-yank beg end type register))

(define-key evil-normal-state-map "Y" 'evil-yank-line-end)

I hope this helps.

Sincerely,

Rafal Kolanski.





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