blob: 90a4486b1a82bb78ec137a251377801609f5cb89 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
;; acl2.el Basic Proof General instance for ACL2
;;
;; Copyright (C) 2000 LFCS Edinburgh.
;;
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; Needs improvement!
;;
;; See the README file in this directory for information.
(require 'proof-easy-config) ; easy configure mechanism
(require 'proof-syntax) ; functions for making regexps
(setq auto-mode-alist ; ACL2 uses two file extensions
(cons ; Only grab .lisp extension after
(cons "\\.lisp$" 'acl2-mode) ; an acl2 file has been loaded
auto-mode-alist))
(proof-easy-config 'acl2 "ACL2"
proof-assistant-home-page "http://www.cs.utexas.edu/users/moore/acl2"
proof-prog-name "acl2"
proof-script-sexp-commands t
proof-comment-start ";"
proof-comment-start ";"
proof-shell-annotated-prompt-regexp "ACL2[ !]*>+"
proof-shell-error-regexp "^Error: "
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-info-command ":help"
;;
;; Syntax table entries for proof scripts (FIXME: incomplete)
;;
proof-script-syntax-table-entries
'(?\[ "(] "
?\] "([ "
?\( "() "
?\) ")( "
?. "w"
?_ "w"
?\' "' "
?` "' "
?, "' "
?\| "."
?\; "< "
?\n "> "
)
;; 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)))
(warn "ACL2 Proof General is incomplete! Please help improve it!
Read the manual, make improvements and send them to feedback@proofgeneral.org")
(provide 'acl2)
|
