9

この質問は、Emacs の Proof General 内で Coq モードを設定することに関するものです。

Emacs に Coq のキーワードと表記を対応する Unicode グリフに自動的に置き換えさせようとしています。funギリシャ語の小文字のラムダ λ や、全称量化記号 ∀ などを定義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 グリフに置き換えることにあると思われますが、よくわかりません。誰かが私のためにこれに光を当てることができますか?

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 に答える