Les glyphes Unicode pour les mots-clés et les opérateurs dans Coq/Proof General sous Emacs

Question

Cette question concerne la configuration du mode Coq dans Proof General, dans Emacs.

J'essaie de faire en sorte qu'Emacs remplace automatiquement les mots-clés et la notation en Coq par les glyphes Unicode correspondants. J'ai réussi à définir fun comme étant le lambda λ minuscule grec, forall comme symbole de quantificateur universel ∀, etc. Je n'ai eu aucun problème à définir des symboles pour les mots.

Le problème est que lorsque je tente de définir des opérateurs =>, ->, <->, etc. à leur symbole Unicode ⇒ → ↔, ils ne sont pas remplacés par les glyphes Unicode correspondant en Coq. Ils sont cependant remplacés dans le tampon *scratch*, lorsque je les teste. J'utilise le même mécanisme pour correspondre Unicode glyps avec la notation Coq:

(defun define-glyph (string char-info) 
    (font-lock-add-keywords 
    nil 
    `((,(format "\\<%s\\>" string) 
     (0 (progn 
     (compose-region 
     (match-beginning 0) (match-end 0) 
     ,(apply #'make-char char-info)) 
     nil)))) 
    )) 

Je soupçonne que le problème est que le mode Coq marque certains signes de ponctuation comme spécial, si Emacs ne tient pas mon code pour les remplacer par les glyphes Unicode, mais je ne suis pas sur. Quelqu'un peut-il s'il vous plaît éclaircir cela pour moi?

Answer 1

Ces opérateurs sont probablement symboles, et non mots, conformément à la table de syntaxe spécifique au mode. Essayez

(defun define-glyph (string char-info) 
    (font-lock-add-keywords 
    nil 
    `((,(format "\\_<%s\\_>" string) 
     (0 (progn 
      (compose-region 
      (match-beginning 0) (match-end 0) 
      ,(apply #'make-char char-info)) 
      nil))))))