==> becomes \<Longigtarrow>rh

m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches

Other

25 stars 5 forks source link

==> becomes \<Longigtarrow>rh #48

Closed gh-salt closed 2 years ago

gh-salt commented 3 years ago

This also affects => (just the h is moved out in that case) and it seems related to #6 but also affects emacs 27.

gh-salt commented 3 years ago

workaround: disable evil-escape-mode

gh-salt commented 3 years ago

The file unicode-token.el from simp-isar-mode appears to be ignored by (my) emacs.

m-fleury commented 3 years ago

For reasons that have yet to be determined this is caused by using both the coq and the isabelle layer in spacemacs*. So a slightly better workaround is removing the coq layer.

From a very quick look at the issue yesterday: a quail function is redefined to support evil-escape-mode. The redefinition is probably lost in that case.

m-fleury commented 2 years ago

in the 2022-RC4 symbols are handled slightly differently. The goal is now composed of symbols instead of unicode, so no replacement is needed anymore.