Glifos Unicode para palabras clave y operadores en Coq/Proof General bajo Emacs

Question

Esta pregunta tiene que ver con la configuración del modo Coq dentro de Proof General, en Emacs.

Estoy intentando que Emacs reemplace automáticamente las palabras clave y la notación en Coq con los glifos Unicode correspondientes. Logré definir fun para que fuera la lambda λ en minúscula griega, forall para ser el símbolo universal del cuantificador ∀, etc. No tuve problemas para definir los símbolos de las palabras.

El problema es que cuando intento de definir operadores =>, ->, <->, etc. a su Unicode símbolo ⇒ → ↔, no se reemplazan por los correspondientes glifos Unicode en Coq. Sin embargo, son reemplazados en el buffer *scratch*, cuando los pruebo. Estoy usando el mismo mecanismo para que coincida con la notación glyps Unicode 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)))) 
    )) 

Sospecho que el problema es que el modo Coq marca ciertos signos de puntuación como algo especial, así que Emacs ignora mi código para reemplazarlos con los glifos Unicode, pero no estoy seguro. ¿Puede alguien por favor arrojar algo de luz sobre esto para mí?

Answer 1

Aquellos operadores son probablemente símbolos, no palabras, de acuerdo con la tabla de sintaxis específica de modo. Pruebe

(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))))))