From 3a4839220f8c620b51236a7831bbe1292f1daf6b Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 21 Mar 2002 16:31:26 +0000
Subject: Greatly improved support.

---
 acl2/acl2.el | 38 +++++++++++++++++++++++++++++++++-----
 1 file changed, 33 insertions(+), 5 deletions(-)

(limited to 'acl2')

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))))
 
 
 
-- 
cgit v1.2.3