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
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
|
;; proof-toolbar.el Toolbar for Proof General
;;
;; David Aspinall <da@dcs.ed.ac.uk>
;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; NB: XEmacs specific code!
;;
;; Toolbar is just for scripting buffer at the moment.
;;
(defcustom proof-toolbar-wanted t
"*Whether to use toolbar in proof mode."
:type 'boolean
:group 'proof-general)
(defconst proof-toolbar-default-button-list
'(proof-toolbar-goal-button
proof-toolbar-retract-button
proof-toolbar-undo-button
proof-toolbar-next-button
proof-toolbar-use-button
proof-toolbar-restart-button
proof-toolbar-qed-button
'[:style 3d]
nil)
"Example value for proof-toolbar-button-list.
This gives a bare toolbar that works for any prover. To add
prover specific buttons, see proof-toolbar.el.")
(defvar proof-toolbar-button-list proof-toolbar-default-button-list
"A toolbar descriptor evaluated in proof-toolbar-setup.
Specifically, a list of sexps which evaluate to entries in a toolbar
descriptor. The default value proof-toolbar-default-button-list
will work for any proof assistant.")
(defvar proof-toolbar nil
"Proof mode toolbar. Set in proof-toolbar-setup.")
(defun proof-toolbar-setup ()
"Initialize proof-toolbar and enable it for the current buffer.
If proof-mode-use-toolbar is nil, change the current buffer toolbar
to the default toolbar."
(if proof-toolbar-wanted
(let
((icontype (if (featurep 'xpm) "xpm" "xbm")))
;; First set the button variables to glyphs.
(mapcar
(lambda (buttons)
(let ((var (car buttons))
(iconfiles (mapcar (lambda (name)
(concat proof-image-directory name
"." icontype)) (cdr buttons))))
(set var (toolbar-make-button-list iconfiles))))
proof-toolbar-iconlist)
;; Now evaluate the toolbar descriptor
(setq proof-toolbar (mapcar 'eval proof-toolbar-button-list))
;; Finally ensure current buffer will display this toolbar
(set-specifier default-toolbar proof-toolbar (current-buffer)))
(set-specifier default-toolbar proof-old-toolbar (current-buffer))))
(defconst proof-old-toolbar default-toolbar
"Saved value of default-toolbar for proofmode.")
;;
;; GENERIC PROOF TOOLBAR BUTTONS
;;
;; Defaults functions are provided below for: up, down, restart
;; Code for specific provers may define the symbols below to use
;; the other buttons: next, prev, goal, qed (images are provided).
;;
;; proof-toolbar-next next function
;; proof-toolbar-next-enable enable predicate for next (or t)
;;
;; etc.
;;
;; To add support for more buttons or alter the default
;; images, proof-toolbar-iconlist should be adjusted.
;;
;;
(defvar proof-toolbar-next-icon nil
"Glyph list for next button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-next-button
[proof-toolbar-next-icon
proof-toolbar-next
(proof-toolbar-next-enable-p)
"Process the next proof command"])
(defvar proof-toolbar-undo-icon nil
"Glyph list for undo button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-undo-button
[proof-toolbar-undo-icon
proof-toolbar-undo
(proof-toolbar-undo-enable-p)
"Undo the previous proof command"])
(defvar proof-toolbar-retract-icon nil
"Glyph list for retract button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-retract-button
[proof-toolbar-retract-icon
proof-toolbar-retract
(proof-toolbar-retract-enable-p)
"Retract buffer"])
(defvar proof-toolbar-use-icon nil
"Glyph list for use button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-use-button
[proof-toolbar-use-icon
proof-toolbar-use
(proof-toolbar-use-enable-p)
"Process whole buffer"])
(defvar proof-toolbar-restart-icon nil
"Glyph list for down button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-restart-button
[proof-toolbar-restart-icon
proof-toolbar-restart
(proof-toolbar-restart-enable-p)
"Restart the proof assistant"])
(defvar proof-toolbar-goal-icon nil
"Glyph list for goal button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-goal-button
[proof-toolbar-goal-icon
proof-toolbar-goal
(proof-toolbar-goal-enable-p)
"Start a new proof"])
(defvar proof-toolbar-qed-icon nil
"Glyph list for QED button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-qed-button
[proof-toolbar-qed-icon
proof-toolbar-qed
(proof-toolbar-qed-enable-p)
"Save proved theorem"])
(defconst proof-toolbar-iconlist
'((proof-toolbar-next-icon "next")
(proof-toolbar-undo-icon "undo")
(proof-toolbar-retract-icon "retract")
(proof-toolbar-use-icon "use")
(proof-toolbar-goal-icon "goal")
(proof-toolbar-qed-icon "qed")
(proof-toolbar-restart-icon "restart"))
"List of icon variable names and their associated image files")
;;
;; GENERIC PROOF TOOLBAR FUNCTIONS
;;
(defun proof-toolbar-process-available-p
"Enabler for toolbar functions.
Checks based on those in proof-check-process-available, but
without giving error messages."
(and (eq proof-buffer-type 'script)
(proof-shell-live-buffer)
(not proof-shell-busy)
;; this last check is wrong for pbp buffer!
(eq proof-script-buffer (current-buffer))))
(defun proof-toolbar-undo-enable-p ()
(and (proof-toolbar-process-available-p)
(proof-locked-end)))
(defun proof-toolbar-undo ()
"Undo last successful in locked region, without deleting it."
(proof-undo-last-successful-command t))
(defun proof-toolbar-next-enable-p ()
;; Could check if there *is* a next command here, to avoid
;; stupid "nothing to do" errors.
t)
(defun proof-toolbar-next ()
"Assert next command in proof to proof process."
(proof-assert-next-command))
(defun proof-toolbar-retract-enable-p ()
(proof-toolbar-process-available-p))
(defun proof-toolbar-retract ()
"Retract buffer."
;; proof-retract-file might be better here!
(goto-char (point-min))
(proof-retract-until-point))
(defun proof-toolbar-use-enable-p ()
;; Could check to see that whole buffer hasn't been
;; processed already.
t)
(defalias 'proof-toolbar-use 'proof-process-buffer)
(defun proof-toolbar-restart-enable-p ()
;; Could disable this unless there's something running.
;; But it's handy to clearup extents, etc, I suppose.
(eq proof-buffer-type 'script))
(defun proof-toolbar-restart ()
(if (yes-or-no-p (concat "Restart " proof-assistant " scripting?"))
(proof-restart-script)))
(defun proof-toolbar-goal-enable-p ()
;; Goals are always allowed: will crank up process if need be.
t)
(defalias 'proof-toolbar-goal 'proof-issue-goal)
;; Actually this should only be available when "no subgoals"
(defun proof-toolbar-qed-enable-p ()
(and proof-shell-proof-completed
(proof-toolbar-process-available-p)))
(defalias 'proof-toolbar-qed 'proof-issue-save)
;;
(provide 'proof-toolbar)
|
