Emacs

2012-04-20 31 views
9

altındaki Coq/Proof General içindeki anahtar sözcükler ve işleçler için Unicode glifleri Bu sorunun Emacs'teki Proof General içindeki Coq modunu yapılandırmakla ilgisi vardır.Emacs

Emacs, Coq'da anahtar sözcükleri ve notasyonları otomatik olarak ilgili Unicode glifleriyle değiştirmeyi deniyorum. fun, Yunan küçük harfli lambda λ, forall evrensel tanımlayıcı sembolü ∀, vb olmak için tanımlamayı başardım. Kelime için sembolleri tanımlamada hiçbir sorun yaşamadım.

sorun onların Unicode sembol an'a → ↔ vb operatörleri =>, ->, <-> tanımlamak çalıştığınızda, onlar Coq gelen Unicode glif değiştirilir olmamasıdır. Ancak, onları test ettiğimde, *scratch* arabelleğindedirler. Ben Coq gösterimi ile Unicode glyps eşleştirmek için aynı mekanizmayı kullanıyorum:

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

Sorun Coq modu özel olarak belirli noktalama işaretleri işaretleri olduğunu sanıyorum, bu yüzden Emacs Unicode glif bunların yerine için kodumu yok sayar, ama emin değilim. Birisi bana bunun için biraz ışık tutabilir mi?

cevap

5

Bu operatörler modu belirli sözdizimi tabloya göre, muhtemelen semboller değil kelime bulunmaktadır.

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