diff options
| -rw-r--r-- | coq-fontlock.el | 15 | ||||
| -rw-r--r-- | coq.el | 10 | ||||
| -rw-r--r-- | proof.el | 14 |
3 files changed, 33 insertions, 6 deletions
diff --git a/coq-fontlock.el b/coq-fontlock.el index b3fbfa98..8f2672c0 100644 --- a/coq-fontlock.el +++ b/coq-fontlock.el @@ -4,6 +4,12 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; $Log$ +;; Revision 1.5 1997/10/30 15:58:29 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; ;; Revision 1.4 1997/10/24 14:51:07 hhg ;; Changed order of "Inversion_clear" and "Inversion" so that former is ;; fontified first. @@ -104,8 +110,11 @@ "EApply" "EAuto" "Elim" +"End" "Exact" +"Exists" "Generalize" +"Grammar" "Hnf" "Induction" "Injection" @@ -116,6 +125,7 @@ "Inversion" "LApply" "Linear" +"Load" "Pattern" "Program" "Prolog" @@ -124,10 +134,13 @@ "Reflexivity" "Replace" "Rewrite" +"Section" "Simplify_eq" "Simpl" "Specialize" +"Split" "Symmetry" +"Syntax" "Tauto" "Transitivity" "Trivial" @@ -149,7 +162,7 @@ ;; ----- regular expressions for font-lock ;; *** To update -(defvar coq-error-regexp "^\\(Error\\|Syntax error\\)" +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)" "A regular expression indicating that the Coq process has identified an error.") @@ -3,6 +3,12 @@ ;; Author: Healfdene Goguen and Thomas Kleymann ;; $Log$ +;; Revision 1.7 1997/10/30 15:58:31 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; ;; Revision 1.6 1997/10/24 14:51:09 hhg ;; Fixed coq-count-undos for comments ;; @@ -481,7 +487,7 @@ proof-shell-start-char ?\372 ; not done proof-shell-end-char ?\373 ; not done proof-shell-field-char ?\374 ; not done - proof-shell-goal-char ?\375 ; done but not working + proof-shell-goal-char ?\375 ; done proof-shell-eager-annotation-start "\376" ; done proof-shell-eager-annotation-end "\377" ; done proof-shell-annotated-prompt-regexp @@ -489,7 +495,7 @@ (char-to-string proof-shell-wakeup-char)) ; done proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" - proof-shell-start-goals-regexp "[0-9]+ subgoal[s]" + proof-shell-start-goals-regexp "[0-9]+ subgoals?" proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp proof-shell-init-cmd coq-process-config proof-shell-config 'coq-shell-adjust-line-width @@ -19,6 +19,12 @@ ;; report ;; $Log$ +;; Revision 1.19 1997/10/30 15:58:33 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; ;; Revision 1.18 1997/10/24 14:51:13 hhg ;; Updated comment about extent types ;; @@ -484,12 +490,11 @@ ;; Proof by pointing ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defconst pbp-goal-command "Pbp %s;" +(defvar pbp-goal-command nil "Command informing the prover that `pbp-button-action' has been requested on a goal.") - -(defconst pbp-hyp-command "PbpHyp %s;" +(defvar pbp-hyp-command nil "Command informing the prover that `pbp-button-action' has been requested on an assumption.") @@ -1197,6 +1202,9 @@ current command." (setq proof-terminal-string (char-to-string proof-terminal-char)) + (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) + (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) + (make-local-variable 'comment-start) (setq comment-start (concat proof-comment-start " ")) (make-local-variable 'comment-end) |