Email Gateway (Aug 19 2022 at 08:26): Email Gateway (Aug 19 2022 at 08:26):From: Makarius <makarius@sketis.net>
Too much Escape-Meta-Alt-Control-Shift can damage your fingers. This is
actually a serious issue that is right now discussed on Coq-club
https://sympa.inria.fr/sympa/arc/coq-club/2012-08/msg00092.html
It refers to general Proof General issues, but it was raised on the Coq
mailing list first.
Makarius
Email Gateway (Aug 19 2022 at 08:26):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
2012-08-29 20:31 Makarius:
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).
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 08:26):From: René Neumann <rene.neumann@in.tum.de>
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.
Thanks,
René
Email Gateway (Aug 19 2022 at 08:27):From: Ramana Kumar <rk436@cam.ac.uk>
On Thu, Aug 30, 2012 at 12:24 PM, René Neumann <rene.neumann@in.tum.de>wrote:
Am 29.08.2012 20:49, schrieb Christoph LANGE:
2012-08-29 20:31 Makarius:
Too much Escape-Meta-Alt-Control-Shift can damage your fingers. This is
actually a serious issue that is right now discussed on Coq-club
https://sympa.inria.fr/sympa/arc/coq-club/2012-08/msg00092.htmlI 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.
One way would be to use vim-like digraphs (ctrl-k /\).
Thanks,
René--
René NeumannInstitut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. MünchenTel: +49-89-289-17232
Office: MI 03.11.055
Email Gateway (Aug 19 2022 at 08:39):From: René Neumann <rene.neumann@in.tum.de>
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)))
Email Gateway (Aug 19 2022 at 08:43):From: Rafal Kolanski <xs@xaph.net>
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.
Last updated: Apr 18 2024 at 08:19 UTC