Unicode-Glyphen für Schlüsselwörter und Operatoren in Coq/Proof Allgemein unter Emacs

Question

Diese Frage hat mit der Konfiguration der Coq-Modus innerhalb Proof Allgemein in Emacs zu tun.

Ich versuche, Emacs automatisch Schlüsselwörter und Notation in Coq mit den entsprechenden Unicode-Glyphen zu ersetzen. Ich habe es geschafft, fun zu definieren, um das griechische Kleinbuchstabenlambda λ zu sein, forall, um das universelle Quantorsymbol ∀ zu sein, usw. Ich hatte keine Probleme, Symbole für Wörter zu definieren.

Das Problem ist, dass wenn ich versuche, Operatoren zu definieren =>, ->, <-> usw. auf ihr Unicode-Symbol ⇒ → ↔, werden sie nicht mit dem entsprechenden Unicode Glyphen in Coq ersetzt. Sie werden jedoch im Puffer *scratch* ersetzt, wenn ich sie teste. Ich bin mit dem gleichen Mechanismus mit Unicode glyps mit Coq Notation zum Spiel:

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

ich das Problem vermuten ist, dass Coq Modus bestimmte Satzzeichen als Sonder markiert, so Emacs ignorieren meinen Code sie mit dem Unicode Glyphen zu ersetzen, aber ich bin mir nicht sicher. Kann mir bitte jemand etwas Licht für mich geben?

Answer 1

Diese Operatoren sind wahrscheinlich Symbole, nicht Wörter, entsprechend der modusspezifischen Syntaxtabelle. Versuchen Sie

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