blob: db3120edcc2a03e4ed22381a838838dc2840dcfd (
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
;;; acl2.el --- Basic Proof General instance for ACL2
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;;; Commentary:
;;
;; Needs improvement!
;;
;; See the README file in this directory for information.
;;; Code:
(require 'proof-easy-config) ; easy configure mechanism
(require 'proof-syntax) ; functions for making regexps
(add-to-list 'auto-mode-alist ; ACL2 uses two file extensions
; Only grab .lisp extension after
(cons "\\.lisp\\'" 'acl2-mode)) ; an acl2 file has been loaded
(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-script-comment-start ";"
proof-shell-annotated-prompt-regexp "ACL2[ !]*>+"
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-quit-cmd ":q" ;; FIXME: followed by C-d.
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)
;;
proof-script-syntax-table-entries
'(?\[ "(] "
?\] "([ "
?\( "() "
?\) ")( "
?. "w "
?_ "w "
?- "w "
?> "w " ;; things treated as names can have > in them
?# "' "
?\' "' "
?` "' "
?, "' "
?\| "."
?\; "< "
?\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 () (if (eq proof-shell-error-or-interrupt-seen 'interrupt)
(proof-shell-insert ":q" nil))))
(warn "ACL2 Proof General is incomplete! Please help improve it!
Please add improvements at https://github.com/ProofGeneral/PG")
(provide 'acl2)
|
