EmacsのCoq/Proofのキーワードと演算子のUnicodeグリフ

Question

この質問は、EmacsのProof General内でCoqモードを設定することと関係しています。

私はEmacsが自動的にCoqのキーワードと表記を対応するUnicodeグリフに置き換えようとしています。私はfunをギリシャの小文字のラムダλ、forallと定義して、ユニバーサル限定記号∀などとしました。私は単語の記号を定義することに問題はありませんでした。

問題は、私は彼らのUnicodeのシンボル⇒→↔になどの演算子=>、->、<->を定義しようとすると、彼らはコックで対応するUnicodeのグリフに置き換えられていないということです。しかし、私はそれらをテストすると、*scratch*バッファに置き換えられます。私はコック表記でのUnicode glypsを一致させるために同じメカニズムを使用しています：

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

私は問題はコックモードは特別として、特定の句読点をマークしていることである疑いがあるので、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))))))