Glifi Unicode per parole chiave e operatori in Coq/Proof General in Emacs

Question

Questa domanda ha a che fare con la configurazione della modalità Coq in Proof General, in Emacs.

Sto cercando di fare in modo che Emacs sostituisca automaticamente le parole chiave e la notazione in Coq con i glifi Unicode corrispondenti. Sono riuscito a definire fun il greco lambda λ minuscolo, forall come il simbolo del quantificatore universale ∀, ecc. Non ho avuto problemi a definire i simboli per le parole.

Il problema è che quando cerco di definire operatori =>, ->, <->, ecc per il loro simbolo ⇒ Unicode → ↔, essi non vengono sostituiti con i corrispondenti glifi Unicode in Coq. Tuttavia, vengono sostituiti nel buffer *scratch* quando li provo. Sto utilizzando lo stesso meccanismo per abbinare glyps Unicode con Coq notazione:

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

Ho il sospetto che il problema è che la modalità Coq segna alcuni segni di punteggiatura come speciali, in modo da Emacs ignora il mio codice di sostituirli con i glifi Unicode, ma non sono sicuro. Per favore qualcuno può far luce su questo per me?

Answer 1

Gli operatori sono probabilmente simboli, non parole, secondo la tabella sintassi specifica modalità. Prova

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