blob: e9924d0e73cad601e48b26cdda8f1e5a7f58a492 (
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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
(require 'proof) ; load generic parts
;; Adjust toolbar entries. (Must be done
;; before proof-toolbar is loaded).
(if proof-running-on-XEmacs (setq af2-toolbar-entries
(remassoc 'context af2-toolbar-entries)))
;; ======== User settings for Af2 ========
;;
;; Defining variables using customize is pretty easy.
;; You should do it at least for your prover-specific user options.
;;
;; proof-site provides us with two customization groups
;; automatically: (based on the name of the assistant)
;;
;; 'af2 - User options for Af2 Proof General
;; 'af2-config - Configuration of Af2 Proof General
;; (constants, but may be nice to tweak)
;;
;; The first group appears in the menu
;; ProofGeneral -> Customize -> Af2
;; The second group appears in the menu:
;; ProofGeneral -> Internals -> Af2 config
;;
(defcustom af2-prog-name "af2 -pg"
"*Name of program to run Af2."
:type 'file
:group 'af2)
(defcustom af2-sym-lock t
"*Whether to use sym-lock or not."
:type 'boolean
:group 'af2)
(defcustom af2-web-page
"http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html"
"URL of web page for Af2."
:type 'string
:group 'af2-config)
(defcustom af2-doc-dir
"/usr/local/doc/af2"
"The name of the root documentation directory for af2."
:type 'string
:group 'af2-config)
(defcustom af2-lib-dir
"/usr/local/lib/af2"
"The name of the root directory for af2 libraries."
:type 'string
:group 'af2-config)
(defcustom af2-tags-program
(concat af2-doc-dir "/tools/af2_etags.sh")
"Program to run to generate TAGS table for proof assistant."
:type 'string
:group 'af2-config)
(defcustom af2-tags-doc
t
"*If non nil, tags table for af2 text documentation is loaded."
:type 'boolean
:group 'af2-config)
(defcustom af2-etags
(concat af2-doc-dir "/tools/af2_etags.sh")
"Command to build tags table."
:type 'string
:group 'af2-config)
(require 'af2-tags)
(require 'af2-outline)
(require 'af2-font)
(require 'af2-fun)
;; ----- Af2 specific menu
(defpgdefault menu-entries
'(
["Delete symbol around cursor" af2-delete-symbol-around-point t]
["Delete symbol" af2-delete-symbol t]
["Compile theorem under cursor" af2-compile-theorem-around-point t]
"----"
("Tags"
["create a tags table for local buffer" af2-tags-create-local-table t]
["------------------" nil nil]
; ["load table" af2-tags-load-table t]
["add table" af2-tags-add-table t]
["add local table" af2-tags-add-local-table t]
["add table for libraries" af2-tags-add-lib-table t]
["add table for text doc" af2-tags-add-doc-table t]
["reset tags table list" af2-tags-reset-table t]
["------------------" nil nil]
["Find theorem, definition ..." find-tag t]
["complete theorem, definition ..." complete-tag t]
)
))
;;
;; ======== Configuration of generic modes ========
;;
(defun af2-config ()
"Configure Proof General scripting for Af2."
(setq
proof-terminal-char ?\. ; ends every command
proof-script-command-end-regexp "[.][ \n\t\r]"
proof-comment-start "(*"
proof-comment-end "*)"
proof-state-command "goals."
proof-goal-command-regexp "goal\\|prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem"
proof-save-command-regexp "save"
proof-goal-with-hole-regexp "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)[ \n\t\r]+\\([^ \n\t\r]+\\)"
proof-save-with-hole-regexp "save[ \n\t\r]+\\(\\([^ \n\t\r]+\\)\\)[ \n\t\r]*\.[ \n\t\r]"
proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror"
proof-non-undoables-regexp "undo"
proof-goal-command "goal %s."
proof-save-command "save %s."
proof-kill-goal-command "abort."
proof-showproof-command "goals."
proof-undo-n-times-cmd "undo %s."
proof-find-and-forget-fn 'af2-find-and-forget
proof-find-theorems-command "search \"%s\"."
proof-auto-multiple-files nil
font-lock-keywords af2-font-lock-keywords
)
)
(defun af2-shell-config ()
"Configure Proof General shell for Af2."
(setq
;proof-shell-cd-cmd "cd \"%s\""
proof-shell-prompt-pattern "\\(>af2> \\)\\|\\(%af2% \\)"
proof-shell-annotated-prompt-regexp "\\(>af2> \\)\\|\\(%af2% \\)"
proof-shell-interrupt-regexp "Interrupt"
proof-shell-start-goals-regexp "^Goals left to prove:"
proof-shell-quit-cmd "quit."
proof-shell-restart-cmd "quit."
proof-shell-proof-completed-regexp "^.*^proved"
))
;;
;; ======== Defining the derived modes ========
;;
;; The name of the script mode is always <proofsym>-script,
;; but the others can be whatever you like.
;;
;; The derived modes set the variables, then call the
;; <mode>-config-done function to complete configuration.
(define-derived-mode af2-mode proof-mode
"Af2 script" nil
(af2-config)
(af2-sym-lock-start)
(proof-config-done)
(af2-setup-outline)
(define-key af2-mode-map [(control j)]
'proof-assert-next-command-interactive)
(define-key af2-mode-map [(control c) (meta d)]
'af2-delete-symbol-around-point)
;; Configure syntax table for block comments
(modify-syntax-entry ?\* ". 23")
(modify-syntax-entry ?\( "()1")
(modify-syntax-entry ?\) ")(4"))
(define-derived-mode af2-shell-mode proof-shell-mode
"Af2 shell" nil
(af2-shell-config)
(proof-shell-config-done))
(define-derived-mode af2-response-mode proof-response-mode
"Af2 response" nil
(proof-response-config-done))
(define-derived-mode af2-goals-mode pbp-mode
"Af2 goals" nil
(af2-sym-lock-start)
(proof-goals-config-done))
;; The response buffer and goals buffer modes defined above are
;; trivial. In fact, we don't need to define them at all -- they
;; would simply default to "proof-response-mode" and "pbp-mode".
;; A more sophisticated instantiation might set font-lock-keywords to
;; add highlighting, or some of the proof by pointing markup
;; configuration for the goals buffer.
;; The final piece of magic here is a hook which configures settings
;; to get the proof shell running. Proof General needs to know the
;; name of the program to run, and the modes for the shell, response,
;; and goals buffers.
(add-hook 'proof-pre-shell-start-hook 'af2-pre-shell-start)
(defun af2-pre-shell-start ()
(setq proof-prog-name af2-prog-name)
(setq proof-mode-for-shell 'af2-shell-mode)
(setq proof-mode-for-response 'af2-response-mode)
(setq proof-mode-for-pbp 'af2-goals-mode))
(provide 'af2)
|
