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
|
;; proof-toolbar.el Toolbar for generic proof mode
;;
;; David Aspinall <da@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; NB: XEmacs specific code!
;;
;; Toolbar is just for scripting mode at the moment.
(defcustom proof-toolbar-wanted t
"*Whether to use toolbar in proof mode."
:type 'boolean
:group 'proof)
(defconst proof-toolbar-bare-button-list
'(proof-toolbar-goal-button
proof-toolbar-up-button
proof-toolbar-down-button
proof-toolbar-restart-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.")
(defconst proof-toolbar-full-button-list
'(proof-toolbar-goal-button
proof-toolbar-up-button
proof-toolbar-down-button
proof-toolbar-restart-button
proof-toolbar-qed-button
proof-toolbar-next-button
proof-toolbar-prev-button
'[:style 3d]
nil)
"Example value for proof-toolbar-button-list.
This button list includes all the buttons which have icons
and hooks provided. Some hooks must be set for prover-specific
functions.")
(defvar proof-toolbar-button-list proof-toolbar-bare-button-list
"A toolbar descriptor evaluated in proof-toolbar-setup.
Specifically, a list of sexps which evaluate to entries in a toolbar
descriptor.")
(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-up-icon nil
"Glyph list for up button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-up-button
[proof-toolbar-up-icon
proof-toolbar-up
proof-toolbar-up-enable
"Undo the previous proof command"])
(defvar proof-toolbar-down-icon nil
"Glyph list for down button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-down-button
[proof-toolbar-down-icon
proof-toolbar-down
proof-toolbar-down-enable
"Process the next proof command"])
(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
"Restart proof scripting"])
(defvar proof-toolbar-next-icon nil
"Glyph list for next level 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
"Display the next level of the proofstate"])
(defvar proof-toolbar-prev-icon nil
"Glyph list for previous level button in proof toolbar.
Initialised in proof-toolbar-setup.")
(defvar proof-toolbar-prev-button
[proof-toolbar-prev-icon
proof-toolbar-prev
proof-toolbar-prev-enable
"Display the prev level of the proofstate"])
(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
"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
"Save proved theorem"])
(defconst proof-toolbar-iconlist
'((proof-toolbar-up-icon "up")
(proof-toolbar-down-icon "down")
(proof-toolbar-next-icon "left")
(proof-toolbar-prev-icon "right")
(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 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))))
(defvar proof-toolbar-up-enable
(lambda ()
(and (proof-toolbar-process-available-p)
(proof-locked-end))))
(defun proof-toolbar-up ()
"Undo last successful in locked region, without deleting it."
(proof-undo-last-successful-command t))
(defvar proof-toolbar-down-enable
;; Could also check if there *is* a next command here,
;; but using proof-segment-up-to can involve tedious parsing.
(lambda ()
(proof-toolbar-process-available-p)))
(defun proof-toolbar-down ()
"Assert next command in proof to proof process."
(proof-assert-next-command))
(defvar proof-toolbar-restart-enable
(lambda () (eq proof-buffer-type 'script)))
;; Something less drastic would be nice!
(defun proof-toolbar-restart ()
(if (yes-or-no-p "Restart proof scripting?")
(proof-restart-script-same-process)))
;; A goal button will need a variable for string to insert,
;; actually.
(defvar proof-toolbar-goal-enable nil)
(defun proof-toolbar-goal ()
(interactive))
;;
(provide 'proof-toolbar)
|
