diff options
| author |  Patrick Loiseleur <da+pg-patrl@inf.ed.ac.uk> | 1999-06-16 16:28:35 +0000 |
|---|---|---|
| committer | Patrick Loiseleur <da+pg-patrl@inf.ed.ac.uk> | 1999-06-16 16:28:35 +0000 |
| commit | 3e10e48dc7833400d84bfbf861f320e7726a0c5a (patch) | |
| tree | 9a5bd6c4df039d228e1cd023dbf70f5851335469 | |
| parent | 43e9156aa0a700ac5090b6c3947c30fb0b793ee0 (diff) | |
better syntax
| -rw-r--r-- | coq/coq-syntax.el | 6 | ||||
| -rw-r--r-- | coq/coq.el | 21 |
2 files changed, 16 insertions, 11 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 93879d9f..fbb1c9f4 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -278,10 +278,10 @@ ;; et pour Definition f [x,y:nat] := body (defconst coq-decl-with-hole-regexp (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) - "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) + "\\)\\s-+\\(" coq-ids "\\)\\s-*[:]")) (defconst coq-defn-with-hole-regexp (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)\\s-*[:[]")) + "\\)\\s-+\\(" coq-id "\\)\\s-*[:]")) (defvar coq-font-lock-keywords-1 (append @@ -310,7 +310,7 @@ (modify-syntax-entry ?< ".") (modify-syntax-entry ?> ".") (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?_ "w") (modify-syntax-entry ?\' "_") (modify-syntax-entry ?\| ".") (modify-syntax-entry ?\* ". 23") @@ -111,16 +111,11 @@ (define-derived-mode coq-shell-mode proof-shell-mode "coq-shell" nil - - (coq-shell-mode-config) - (setq font-lock-keywords coq-font-lock-keywords-1) - (font-lock-mode)) + (coq-shell-mode-config)) (define-derived-mode coq-response-mode proof-response-mode "CoqResp" nil - (setq font-lock-keywords coq-font-lock-terms) - (coq-init-syntax-table) - (proof-response-config-done)) + (coq-response-config)) (define-derived-mode coq-mode proof-mode "coq" nil @@ -496,11 +491,21 @@ ) (coq-init-syntax-table) + (setq font-lock-keywords coq-font-lock-keywords-1) (proof-shell-config-done)) (defun coq-pbp-mode-config () (setq pbp-change-goal "Show %s.") - (setq pbp-error-regexp coq-error-regexp)) + (setq pbp-error-regexp coq-error-regexp) + + (coq-init-syntax-table) + (setq font-lock-keywords coq-font-lock-keywords-1) + (proof-font-lock-minor-mode)) + +(defun coq-response-config () + (coq-init-syntax-table) + (setq font-lock-keywords coq-font-lock-keywords-1) + (proof-response-config-done)) (provide 'coq) |