diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1999-02-03 15:55:42 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1999-02-03 15:55:42 +0000 |
| commit | 113a83d751f3fc51fc6fc6655e3ee77f488b2793 (patch) | |
| tree | 1ef34cc2d8dc80237684c187d381cbc29fb6d334 | |
| parent | c28be95727fe2023d2937958ac53aa1716958337 (diff) | |
fixed syntax entry for "_"
| -rw-r--r-- | coq/coq.el | 5 | ||||
| -rw-r--r-- | isa/isa.el | 5 | ||||
| -rw-r--r-- | lego/lego-syntax.el | 10 | ||||
| -rw-r--r-- | lego/lego.el | 13 |
4 files changed, 12 insertions, 21 deletions
@@ -309,10 +309,7 @@ (setq proof-mode-for-pbp 'coq-pbp-mode) ) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Configuring proof and pbp mode and setting up various utilities ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - +; FIXME: IMHO (tms) this ought to be defined in coq-syntax and not here. (defun coq-init-syntax-table () "Set appropriate values for syntax table in current buffer." @@ -609,10 +609,7 @@ Resulting output from Isabelle will be parsed by Proof General." (setq proof-mode-for-shell 'isa-shell-mode) (setq proof-mode-for-pbp 'isa-pbp-mode)) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Configuring proof and pbp mode and setting up various utilities ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - +; FIXME: IMHO (tms) this ought to be defined in isa-syntax and not here. (defun isa-init-syntax-table () "Set appropriate values for syntax table in current buffer." (modify-syntax-entry ?\$ ".") diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index a49ee574..9feb283a 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -100,4 +100,14 @@ (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face) (list lego-save-with-hole-regexp 2 'font-lock-function-name-face)))) +(defun lego-init-syntax-table () + "Set appropriate values for syntax table in current buffer." + + (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4")) + (provide 'lego-syntax) diff --git a/lego/lego.el b/lego/lego.el index 5711a000..5b34d6bc 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -338,19 +338,6 @@ Checks the width in the `proof-goals-buffer'" proof-mode-for-response 'lego-response-mode proof-mode-for-pbp 'lego-pbp-mode)) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Configuring proof and pbp mode and setting up various utilities ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun lego-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?_ "w") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - (modify-syntax-entry ?\* ". 23") - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) (defun lego-mode-config () |