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

Question

此问题与在Emacs中的Proof General中配置Coq模式有关.

我正在尝试让Emacs使用相应的Unicode字形自动替换Coq中的关键字和符号.我设法定义fun为希腊小写lambdaλ,forall作为通用量词符号∀等.我没有问题定义单词的符号.

问题是,当我尝试定义操作符=>,->,<->等他们的Unicode符号⇒→↔,他们不是在勒柯克相应的Unicode字形所取代.但是,*scratch*当我测试它们时,它们会在缓冲区中被替换.我使用相同的机制将Unicode glyps与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字形替换它们,但我不确定.有人可以帮我解释一下吗？

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