9

这个问题与在 Emacs 中的 Proof General 中配置 Coq 模式有关。

我试图让 Emacs 用相应的 Unicode 字形自动替换 Coq 中的关键字和符号。我设法将其定义fun为希腊小写 lambda λ、forall通用量词符号 ∀ 等。我在定义单词符号时没有遇到任何问题。

问题是当我尝试为它们的 Unicode 符号 ⇒→↔ 定义运算符=>时->，<->它们不会被 Coq 中相应的 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 字形，但我不确定。有人可以为我解释一下吗？

4

1 回答 1

5

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

(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))))))
于 2012-04-21T00:10:23.413 回答