Symbols typed using XCompose not replaced

[Mesabloo]

The Isabelle mode provides a few shortcuts (such as => for \<Rightarrow>) which are all within isar-unicode-tokens.el. However, it seems that this does not work well with using a XCompose layer.

We may need to take a look here.

[Mesabloo]

After some research, it seems that Quail is unable to handle UTF8 characters (any multi-byte character). However, I have found that remapping unicode characters to the equivalent Isabelle format[^1] seems to work. Here's an extract from my config:

(define-minor-mode isar--insert-unicode-minor-mode
  "A minor mode to translate inserted unicode characters into the isabelle format (e.g. ⇒ to \\<Rightarrow>)."
  :keymap (let ((map (make-sparse-keymap))) 
            (define-key map (kbd "⇒") "\\<Rightarrow>")
            (define-key map (kbd "×") "\\<times>")
            (define-key map (kbd "∈") "\\<in>")
            (define-key map (kbd "∀") "\\<forall>")
            (define-key map (kbd "∃") "\\<exists>")
            (define-key map (kbd "→") "\\<rightarrow>")
            (define-key map (kbd "←") "\\<leftarrow>")
            (define-key map (kbd "↓") "\\<downarrow>")
            (define-key map (kbd "↑") "\\<uparrow>")
            ;; Map a lot more Unicode characters...
            map))

(add-hook! 'isar-mode-hook 'isar--insert-unicode-minor-mode)

I'm not really sure whether this is ugly or not, but at least this seems to work fine (careful about add-hook!, I believe it comes from Doom).

[^1]: Solution found here: https://emacs.stackexchange.com/a/39073

[m-fleury]

I think that you can also use the isar-mode-map map instead of creating a new map, but I have not tried it.

[Mesabloo]

This is true, I completely forgot about isar-mode-map. :sweat_smile: This seems to work fine (dropped the minor mode and used isar-mode-map instead of a new sparse keymap):

;; Map a few unicode tokens to their Isabelle equivalents.
(after! isar-mode
  (define-key isar-mode-map (kbd "⇒") "\\<Rightarrow>")
  (define-key isar-mode-map (kbd "×") "\\<times>")
  (define-key isar-mode-map (kbd "∈") "\\<in>")
  (define-key isar-mode-map (kbd "∀") "\\<forall>")
  (define-key isar-mode-map (kbd "∃") "\\<exists>")
  (define-key isar-mode-map (kbd "→") "\\<rightarrow>")
  (define-key isar-mode-map (kbd "←") "\\<leftarrow>")
  (define-key isar-mode-map (kbd "↓") "\\<downarrow>")
  (define-key isar-mode-map (kbd "↑") "\\<uparrow>")
  (define-key isar-mode-map (kbd "↦") "\\<mapsto>")
  (define-key isar-mode-map (kbd "≡") "\\<equiv>")
  (define-key isar-mode-map (kbd "≢") "\\<notequiv>")
  (define-key isar-mode-map (kbd "∧") "\\<and>")
  (define-key isar-mode-map (kbd "∨") "\\<or>")
  (define-key isar-mode-map (kbd "¬") "\\<not>") 
  (define-key isar-mode-map (kbd "≠") "\\<noteq>")
  (define-key isar-mode-map (kbd "λ") "\\<lambda>")
  ;; Map other Unicode characters as needed...
)

[m-fleury]

I think that a slightly more robust version (and less hand-copy-paste to avoid listing all characters) is:

(cl-loop for (token beautified) in (cl-concatenate 'list isar-extended-symbols-tokens isar-symbols-tokens ...)
     do  (define-key isar-mode-map (kbd beautified) (format "\\<%s>" token)))

(but this is untested… and you need to replace the ... by the list of all tokens in isar-mode)

[Mesabloo]

The two lists isar-extended-symbols-tokens isar-symbols-tokens seem to be enough. All other lists either use custom attributes (which may not work in such loop, although I did not test it) or are included within those two. This works fine though! I just need to make some adjustments either to the tokens used in the isar mode, or my XCompose layer (for example, they do not agree on ⦅ ⦆ because the isar mode uses ⦇ ⦈; the former are white parentheses, while the latter are Z-notation image brackets), but this is a bit unrelated to the issue.