diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-03-21 16:31:26 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-03-21 16:31:26 +0000 |
| commit | 3a4839220f8c620b51236a7831bbe1292f1daf6b (patch) | |
| tree | cd606af6ee297f97a27afbb55ff71b68e09ab213 /acl2 | |
| parent | 9f84867ebb296649db1656106910ee2527385aaa (diff) | |
Greatly improved support.
Diffstat (limited to 'acl2')
| -rw-r--r-- | acl2/acl2.el | 38 |
1 files changed, 33 insertions, 5 deletions
diff --git a/acl2/acl2.el b/acl2/acl2.el index 90a4486b..d78084cd 100644 --- a/acl2/acl2.el +++ b/acl2/acl2.el @@ -29,13 +29,24 @@ proof-shell-annotated-prompt-regexp "ACL2[ !]*>+" - proof-shell-error-regexp "^Error: " + proof-save-command-regexp "(def\\w+\\s " + proof-goal-command-regexp "(def\\w+\\s " + proof-save-with-hole-regexp "(def\\w+[ \t\n]+\\(\\w+\\)" + proof-save-with-hole-result 1 + proof-shell-error-regexp + "^Error: \\|Error in TOP-LEVEL: \\|\\*\\*\\*\\* FAILED \\*\\*\\*" proof-shell-interrupt-regexp "Correctable error: Console interrupt." proof-shell-prompt-pattern "ACL2[ !]*>+" proof-shell-quit-cmd ":q" ;; FIXME: followed by C-d. - proof-shell-restart-cmd "#." ;; FIXME: maybe not? + proof-shell-restart-cmd ":q\n:q\n:q\n(lp)\n" ;; FIXME: maybe not? proof-info-command ":help" + proof-undo-n-times-cmd ":ubt %s" ;; shouldn't give errors + proof-forget-id-command ":ubt %s" ;; so use ubt not ubt! + proof-context-command ":pbt :max" + ;; proof-showproof-cmd ":pbt :here" + + proof-shell-truncate-before-error nil ;; ;; Syntax table entries for proof scripts (FIXME: incomplete) @@ -45,8 +56,11 @@ ?\] "([ " ?\( "() " ?\) ")( " - ?. "w" - ?_ "w" + ?. "w " + ?_ "w " + ?- "w " + ?> "w " ;; things treated as names can have > in them + ?# "' " ?\' "' " ?` "' " ?, "' " @@ -55,13 +69,27 @@ ?\n "> " ) + ;; A tiny bit of syntax highlighting + ;; + proof-script-font-lock-keywords + (append + (list + (proof-ids-to-regexp '("defthm" "defabbrev" "defaxiom" "defchoose" + "defcong" "defconst" "defdoc" "defequiv" + "defevaluator" "defpackage" "deflabel" "deftheory" + "implies" "equal" "and"))) + (if (boundp 'lisp-font-lock-keywords) ;; wins if font-lock is loaded + lisp-font-lock-keywords)) + + ;; End of easy config. ) ;; Interrupts and errors enter another loop; break out of it (add-hook 'proof-shell-handle-error-or-interrupt-hook - (lambda () (proof-shell-insert ":q" nil))) + (lambda () (if (eq proof-shell-error-or-interrupt-seen 'interrupt) + (proof-shell-insert ":q" nil)))) |