Emacs下Coq/Proof General关键字和运算符的Unicode字形

Question

这个问题涉及到在Emacs中配置Proof General中的Coq模式。我试图让Emacs自动将Coq中的关键词和符号替换为相应的Unicode字符。我成功地将fun定义为希腊小写字母lambda λ，将forall定义为全称量词符号∀等。我已经成功地为单词定义了符号。

问题在于，当我尝试将运算符=>、->、<->等定义为它们的Unicode符号⇒→↔时，在Coq中它们没有被替换为相应的Unicode字符。但是，当我在*scratch*缓冲区中测试它们时，它们被替换了。我使用相同的机制来匹配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))))
   ))

我猜测问题出在Coq模式将某些标点符号标记为特殊字符，因此Emacs忽略我的代码以替换它们为Unicode字形，但我不确定。可以有人为我解释一下吗？

- Mayer Goldberg

Answer 1

那些运算符可能是“符号”，而不是“单词”，根据特定模式的语法表。请尝试。

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

- huaiyuan