diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-01 19:24:34 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-01 19:24:34 +0000 |
| commit | c25e3c1a1c3c12a81f90b0a20321ca9734634032 (patch) | |
| tree | c9f28dc5bdde334f820253ec8276856643b74119 /lego/lego.el | |
| parent | 00c337af2ea574baf01a26581b80aa1fd955e2f0 (diff) | |
o added support for byte-compilation
o removed hhg tags in todo
o fixed font-lock for FSF Emacs 20.2
o ensured that goals buffer is updated for longer queues
o fixed a bug in proof-universal-keys-only-mode
Diffstat (limited to 'lego/lego.el')
| -rw-r--r-- | lego/lego.el | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/lego/lego.el b/lego/lego.el index 3674979d..a1c5b234 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -135,15 +135,15 @@ "*Regular expression indicating that the proof has been completed.") (defvar lego-save-command-regexp - (concat "^" (ids-to-regexp lego-keywords-save))) + (concat "^" (proof-ids-to-regexp lego-keywords-save))) (defvar lego-goal-command-regexp - (concat "^" (ids-to-regexp lego-keywords-goal))) + (concat "^" (proof-ids-to-regexp lego-keywords-goal))) (defvar lego-kill-goal-command "KillRef;") (defvar lego-forget-id-command "Forget ") (defvar lego-undoable-commands-regexp - (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal" + (proof-ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal" "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption" "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI" "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed" @@ -155,7 +155,7 @@ (defvar lego-outline-regexp (concat "[[*]\\|" - (ids-to-regexp + (proof-ids-to-regexp '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive" "Unfreeze")))) @@ -184,6 +184,7 @@ (define-derived-mode lego-response-mode proof-response-mode "LEGOResp" nil (setq font-lock-keywords lego-font-lock-terms) + (lego-init-syntax-table) (proof-response-config-done))) (define-derived-mode lego-pbp-mode pbp-mode @@ -410,7 +411,7 @@ proof-save-with-hole-regexp lego-save-with-hole-regexp proof-goal-with-hole-regexp lego-goal-with-hole-regexp proof-kill-goal-command lego-kill-goal-command - proof-commands-regexp (ids-to-regexp lego-commands)) + proof-commands-regexp (proof-ids-to-regexp lego-commands)) (lego-init-syntax-table) @@ -537,6 +538,7 @@ We assume that module identifiers coincide with file names." (setq pbp-change-goal "Next %s;" pbp-error-regexp lego-error-regexp) (setq font-lock-keywords lego-font-lock-terms) + (lego-init-syntax-table) (proof-goals-config-done)) |