1 | ;; pg-goals.el Proof General goals buffer mode. |
---|
2 | ;; |
---|
3 | ;; Copyright (C) 1994-2002 LFCS Edinburgh. |
---|
4 | ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, |
---|
5 | ;; Thomas Kleymann and Dilip Sequeira |
---|
6 | ;; License: GPL (GNU GENERAL PUBLIC LICENSE) |
---|
7 | ;; |
---|
8 | ;; pg-goals.el,v 8.3 2006/09/24 15:05:35 da Exp |
---|
9 | ;; |
---|
10 | |
---|
11 | ;; A sub-module of proof-shell; assumes proof-script loaded. |
---|
12 | (require 'pg-assoc) |
---|
13 | |
---|
14 | (require 'bufhist) |
---|
15 | |
---|
16 | ;; Nuke some byte compiler warnings. |
---|
17 | (eval-when-compile |
---|
18 | (require 'easymenu)) |
---|
19 | |
---|
20 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
21 | ;; |
---|
22 | ;; Goals buffer mode |
---|
23 | ;; |
---|
24 | |
---|
25 | ;; |
---|
26 | ;; The mode itself |
---|
27 | ;; |
---|
28 | (eval-and-compile ; to define proof-goals-mode-map |
---|
29 | (define-derived-mode proof-goals-mode proof-universal-keys-only-mode |
---|
30 | proof-general-name |
---|
31 | "Mode for goals display. |
---|
32 | May enable proof-by-pointing or similar features. |
---|
33 | \\{proof-goals-mode-map}" |
---|
34 | (setq proof-buffer-type 'goals) |
---|
35 | ;; font-lock-keywords isn't automatically buffer-local in Emacs 21.2 |
---|
36 | (make-local-variable 'font-lock-keywords) |
---|
37 | (make-local-hook 'kill-buffer-hook) |
---|
38 | (add-hook 'kill-buffer-hook 'pg-save-from-death nil t) |
---|
39 | (easy-menu-add proof-goals-mode-menu proof-goals-mode-map) |
---|
40 | (easy-menu-add proof-assistant-menu proof-goals-mode-map) |
---|
41 | (proof-toolbar-setup) |
---|
42 | (erase-buffer) |
---|
43 | (buffer-disable-undo) |
---|
44 | (if proof-keep-response-history (bufhist-mode)) ; history for contents |
---|
45 | (set-buffer-modified-p nil))) |
---|
46 | |
---|
47 | ;; |
---|
48 | ;; Keys for goals buffer |
---|
49 | ;; |
---|
50 | (define-key proof-goals-mode-map [q] 'bury-buffer) |
---|
51 | (cond |
---|
52 | (proof-running-on-XEmacs |
---|
53 | (define-key proof-goals-mode-map [(button2)] 'pg-goals-button-action) |
---|
54 | (define-key proof-goals-mode-map [(control button2)] 'proof-undo-and-delete-last-successful-command) |
---|
55 | ;; button 2 is a nuisance on 2 button mice, so we'll do 1 as well. |
---|
56 | ;; Actually we better hadn't, people like to use it for cut and paste. |
---|
57 | ;; (define-key proof-goals-mode-map [(button1)] 'pg-goals-button-action) |
---|
58 | ;; (define-key proof-goals-mode-map [(control button1)] 'proof-undo-and-delete-last-successful-command) |
---|
59 | ;; C Raffalli: The next key on button3 will be remapped to proof by contextual |
---|
60 | ;; menu by pg-pbrpm.el. In this case, control button3 is mapped to |
---|
61 | ;; 'pg-goals-yank-subterm |
---|
62 | (define-key proof-goals-mode-map [(button3)] 'pg-goals-yank-subterm)) |
---|
63 | (t |
---|
64 | (define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action) |
---|
65 | (define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command) |
---|
66 | ;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action) |
---|
67 | ;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command) |
---|
68 | ;; C Raffalli: The next key on button3 will be remapped to proof by contextual |
---|
69 | ;; menu by pg-pbrpm.el. In this cans, control button3 is mapped to |
---|
70 | ;; 'pg-goals-yank-subterm |
---|
71 | (define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm))) |
---|
72 | |
---|
73 | |
---|
74 | ;; |
---|
75 | ;; Menu for goals buffer |
---|
76 | ;; |
---|
77 | (easy-menu-define proof-goals-mode-menu |
---|
78 | proof-goals-mode-map |
---|
79 | "Menu for Proof General goals buffer." |
---|
80 | proof-aux-menu) |
---|
81 | |
---|
82 | |
---|
83 | ;; |
---|
84 | ;; The completion of init |
---|
85 | ;; |
---|
86 | (defun proof-goals-config-done () |
---|
87 | "Initialise the goals buffer after the child has been configured." |
---|
88 | (proof-font-lock-configure-defaults nil) |
---|
89 | (proof-x-symbol-config-output-buffer)) |
---|
90 | |
---|
91 | |
---|
92 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
93 | ;; |
---|
94 | ;; Goals buffer processing |
---|
95 | ;; |
---|
96 | (defun pg-goals-display (string) |
---|
97 | "Display STRING in the proof-goals-buffer, properly marked up. |
---|
98 | Converts term substructure markup into mouse-highlighted extents, |
---|
99 | and properly fontifies STRING using proof-fontify-region." |
---|
100 | (save-excursion |
---|
101 | ;; Response buffer may be out of date. It may contain (error) |
---|
102 | ;; messages relating to earlier proof states |
---|
103 | |
---|
104 | ;; FIXME da: this isn't always the case. In Isabelle |
---|
105 | ;; we get <WARNING MESSAGE> <CURRENT GOALS> output, |
---|
106 | ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>. Both times |
---|
107 | ;; <WARNING MESSAGE> would be relevant. |
---|
108 | ;; We should only clear the output that was displayed from |
---|
109 | ;; the *previous* prompt. |
---|
110 | |
---|
111 | ;; Erase the response buffer if need be, maybe removing the |
---|
112 | ;; window. Indicate it should be erased before the next output. |
---|
113 | (proof-shell-maybe-erase-response t t) |
---|
114 | |
---|
115 | ;; Erase the goals buffer and add in the new string |
---|
116 | (set-buffer proof-goals-buffer) |
---|
117 | |
---|
118 | (unless (eq 0 (buffer-size)) |
---|
119 | (bufhist-checkpoint-and-erase)) |
---|
120 | ;; Only bother processing and displaying, etc, if string is |
---|
121 | ;; non-empty. |
---|
122 | (unless (string-equal string "") |
---|
123 | (insert string) |
---|
124 | |
---|
125 | (if pg-use-specials-for-fontify |
---|
126 | ;; With special chars for fontification, do that first, |
---|
127 | ;; but keep specials in case also used for subterm markup. |
---|
128 | (proof-fontify-region (point-min) (point-max) 'keepspecials)) |
---|
129 | (pg-goals-analyse-structure (point-min) (point-max)) |
---|
130 | |
---|
131 | (unless pg-use-specials-for-fontify |
---|
132 | ;; provers which use ordinary keywords to fontify output must |
---|
133 | ;; do fontification second after subterm specials are removed. |
---|
134 | (proof-fontify-region (point-min) (point-max))) |
---|
135 | |
---|
136 | ;; Record a cleaned up version of output string |
---|
137 | (setq proof-shell-last-output |
---|
138 | (buffer-substring (point-min) (point-max))) |
---|
139 | |
---|
140 | (set-buffer-modified-p nil) ; nicety |
---|
141 | |
---|
142 | ;; Keep point at the start of the buffer. |
---|
143 | (proof-display-and-keep-buffer |
---|
144 | proof-goals-buffer "=========")))) |
---|
145 | |
---|
146 | |
---|
147 | (defun pg-goals-analyse-structure (start end) |
---|
148 | "Analyse the region between START and END for subterm and PBP markup. |
---|
149 | |
---|
150 | For subterms, we can make nested regions in the concrete syntax into |
---|
151 | active mouse-highlighting regions, each of which can be used to |
---|
152 | communicate a selected term back to the prover. The output text is |
---|
153 | marked up with the annotation scheme: |
---|
154 | |
---|
155 | [ <annotation> | <subterm/concrete> ] |
---|
156 | |
---|
157 | ^ ^ ^ |
---|
158 | | | | |
---|
159 | pg-subterm-start-char pg-subterm-sep-char pg-subterm-end-char |
---|
160 | |
---|
161 | The annotation is intended to indicate a node in the abstract syntax |
---|
162 | tree inside the prover, which can be used to pick out the internal |
---|
163 | representation of the term itself. We assume that the annotation |
---|
164 | takes the form of a sequence of characters: |
---|
165 | |
---|
166 | <length of shared prefix previous> <ann1> <ann2> .. <annN> |
---|
167 | |
---|
168 | Where each element <..> is a character which is *less* than |
---|
169 | pg-subterm-first-special-char, but *greater* than 128. Each |
---|
170 | character code has 128 subtracted to yield a number. The first |
---|
171 | character allows a simple optimisation by sharing a prefix of |
---|
172 | the previous (left-to-right) subterm's annotation. (See the |
---|
173 | variable `pg-subterm-anns-use-stack' for an alternative |
---|
174 | optimisation.) |
---|
175 | |
---|
176 | For subterm markup without communication back to the prover, the |
---|
177 | annotation is not needed, but the first character must still be given. |
---|
178 | |
---|
179 | For proof-by-pointing (PBP) oriented markup, `pg-topterm-char' and |
---|
180 | `pg-topterm-goalhyp-fn' should be set. Together these allow |
---|
181 | further active regions to be defined, corresponding to \"top elements\" |
---|
182 | in the proof-state display. A \"top element\" is currently assumed |
---|
183 | to be either a hypothesis or a subgoal, and is assumed to occupy |
---|
184 | a line (or at least a line). The markup is simply |
---|
185 | |
---|
186 | & <goal or hypthesis line in proof state> |
---|
187 | ^ |
---|
188 | | |
---|
189 | pg-topterm-char |
---|
190 | |
---|
191 | And the function `pg-topterm-goalhyp-fn' is called to do the |
---|
192 | further analysis, to return an indication of the goal/hyp and |
---|
193 | record a name value. These values are used to construct PBP |
---|
194 | commands which can be sent to the prover." |
---|
195 | (if pg-subterm-start-char |
---|
196 | (let* |
---|
197 | ((cur start) |
---|
198 | (len (- end start)) |
---|
199 | (ann (make-string len ?x)) ; (more than) enough space for longest ann'n |
---|
200 | (ap 0) |
---|
201 | c stack topl span) |
---|
202 | |
---|
203 | (while (< cur end) |
---|
204 | (setq c (char-after cur)) |
---|
205 | (cond |
---|
206 | ;; Seen goal char: this is the start of a top extent |
---|
207 | ;; (assumption or goal) |
---|
208 | ((= c pg-topterm-char) |
---|
209 | (setq topl (cons cur topl)) |
---|
210 | (setq ap 0)) |
---|
211 | |
---|
212 | ;; Seen subterm start char: it's followed by a char |
---|
213 | ;; indicating the length of the annotation prefix |
---|
214 | ;; which can be shared with the previous subterm. |
---|
215 | ((= c pg-subterm-start-char) |
---|
216 | (incf cur) |
---|
217 | (if pg-subterm-anns-use-stack |
---|
218 | (setq ap (- ap (- (char-after cur) 128))) |
---|
219 | (setq ap (- (char-after cur) 128))) |
---|
220 | (incf cur) |
---|
221 | ;; Now search for a matching end-annotation char, recording the |
---|
222 | ;; annotation found. |
---|
223 | (while (not (= (setq c (char-after cur)) pg-subterm-sep-char)) |
---|
224 | (aset ann ap (- c 128)) |
---|
225 | (incf ap) |
---|
226 | (incf cur)) |
---|
227 | ;; Push the buffer pos and annotation |
---|
228 | (setq stack (cons cur |
---|
229 | (cons (substring ann 0 ap) stack)))) |
---|
230 | |
---|
231 | ;; Seen a subterm end char, terminating an annotated region |
---|
232 | ;; in the concrete syntax. We make a highlighting span now. |
---|
233 | ((and (consp stack) (= c pg-subterm-end-char)) |
---|
234 | ;; (consp stack) added to make the code more robust. |
---|
235 | ;; [ Condition violated with lego/example.l and GNU Emacs 20.3 ] |
---|
236 | (setq span (make-span (car stack) cur)) |
---|
237 | (set-span-property span 'mouse-face 'highlight) |
---|
238 | (set-span-property span 'goalsave (cadr stack));; FIXME: 'goalsave? |
---|
239 | ;; (set-span-property span 'balloon-help helpmsg) |
---|
240 | (set-span-property span 'help-echo 'pg-goals-get-subterm-help) |
---|
241 | (if pg-subterm-anns-use-stack |
---|
242 | ;; Pop annotation off stack |
---|
243 | (progn |
---|
244 | (setq ap 0) |
---|
245 | (while (< ap (length (cadr stack))) |
---|
246 | (aset ann ap (aref (cadr stack) ap)) |
---|
247 | (incf ap)))) |
---|
248 | ;; Finish popping annotations |
---|
249 | (setq stack (cdr (cdr stack))))) |
---|
250 | ;; On to next char |
---|
251 | (incf cur)) |
---|
252 | |
---|
253 | ;; List of topterm beginning positions (goals/hyps) found |
---|
254 | (setq topl (reverse (cons end topl))) |
---|
255 | |
---|
256 | ;; Proof-by-pointing markup assumes "top" elements which define a |
---|
257 | ;; context for a marked-up (sub)term: we assume these contexts to |
---|
258 | ;; be either a subgoal to be solved or a hypothesis. |
---|
259 | ;; Top element spans are only made if pg-topterm-goalhyp-fn is set. |
---|
260 | ;; NB: If we want Coq pbp: (setq coq-current-goal 1) |
---|
261 | (if pg-topterm-goalhyp-fn |
---|
262 | (while (setq ap (car topl) |
---|
263 | topl (cdr topl)) |
---|
264 | (pg-goals-make-top-span ap (car topl)))) |
---|
265 | |
---|
266 | ;; Finally: strip the specials. This should |
---|
267 | ;; leave the spans in exactly the right place. |
---|
268 | (pg-assoc-strip-subterm-markup-buf start end)))) |
---|
269 | |
---|
270 | |
---|
271 | (defun pg-goals-make-top-span (start end) |
---|
272 | "Make a top span (goal/hyp area) for mouse active output." |
---|
273 | (let (span typname) |
---|
274 | (goto-char start) |
---|
275 | ;; skip the pg-topterm-char itself |
---|
276 | (forward-char) |
---|
277 | ;; typname is expected to be a cons-cell of a type (goal/hyp) |
---|
278 | ;; with a name, retrieved from the text immediately following |
---|
279 | ;; the topterm-char annotation. |
---|
280 | (setq typname (funcall pg-topterm-goalhyp-fn)) |
---|
281 | (beginning-of-line) ;; any reason why? |
---|
282 | (setq start (point)) |
---|
283 | (goto-char end) |
---|
284 | (beginning-of-line) |
---|
285 | (backward-char) |
---|
286 | (setq span (make-span start (point))) |
---|
287 | (set-span-property span 'mouse-face 'highlight) |
---|
288 | (set-span-property span 'proof-top-element typname))) |
---|
289 | |
---|
290 | |
---|
291 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
292 | ;; |
---|
293 | ;; Commands to prover based on subterm markup (inc PBP). |
---|
294 | ;; |
---|
295 | ;; |
---|
296 | |
---|
297 | ;; Fairly specific to the mechanism implemented in LEGO |
---|
298 | ;; To make (more) sense of this code, you should read the |
---|
299 | ;; relevant LFCS tech report by tms, yb, and djs |
---|
300 | |
---|
301 | (defun pg-goals-yank-subterm (event) |
---|
302 | "Copy the subterm indicated by the mouse-click EVENT. |
---|
303 | This function should be bound to a mouse button in the Proof General |
---|
304 | goals buffer. |
---|
305 | |
---|
306 | The EVENT is used to find the smallest subterm around a point. The |
---|
307 | subterm is copied to the kill-ring, and immediately yanked (copied) |
---|
308 | into the current buffer at the current cursor position. |
---|
309 | |
---|
310 | In case the current buffer is the goals buffer itself, the yank |
---|
311 | is not performed. Then the subterm can be retrieved later by an |
---|
312 | explicit yank." |
---|
313 | (interactive "e") |
---|
314 | (let (span) |
---|
315 | (save-window-excursion |
---|
316 | (save-excursion |
---|
317 | (mouse-set-point event) |
---|
318 | ;; Get either the proof body or whole goalsave |
---|
319 | (setq span (or |
---|
320 | (span-at (point) 'proof) |
---|
321 | (span-at (point) 'goalsave))) |
---|
322 | (if span (copy-region-as-kill |
---|
323 | (span-start span) |
---|
324 | (span-end span))))) |
---|
325 | (if (and span (not (eq proof-buffer-type 'goals))) |
---|
326 | (yank)))) |
---|
327 | |
---|
328 | (defun pg-goals-button-action (event) |
---|
329 | "Construct a proof-by-pointing command based on the mouse-click EVENT. |
---|
330 | This function should be bound to a mouse button in the Proof General |
---|
331 | goals buffer. |
---|
332 | |
---|
333 | The EVENT is used to find the smallest subterm around a point. A |
---|
334 | position code for the subterm is sent to the proof assistant, to ask |
---|
335 | it to construct an appropriate proof command. The command which is |
---|
336 | constructed will be inserted at the end of the locked region in the |
---|
337 | proof script buffer, and immediately sent back to the proof assistant. |
---|
338 | If it succeeds, the locked region will be extended to cover the |
---|
339 | proof-by-pointing command, just as for any proof command the |
---|
340 | user types by hand." |
---|
341 | (interactive "e") |
---|
342 | (mouse-set-point event) |
---|
343 | (pg-goals-construct-command)) |
---|
344 | |
---|
345 | ;; Using the spans in a mouse behavior is quite simple: from the mouse |
---|
346 | ;; position, find the relevant span, then get its annotation and |
---|
347 | ;; produce a piece of text that will be inserted in the right buffer. |
---|
348 | |
---|
349 | (defun proof-expand-path (string) |
---|
350 | (let ((a 0) (l (length string)) ls) |
---|
351 | (while (< a l) |
---|
352 | (setq ls (cons (int-to-string |
---|
353 | (char-to-int (aref string a))) |
---|
354 | (cons " " ls))) |
---|
355 | (incf a)) |
---|
356 | (apply 'concat (nreverse ls)))) |
---|
357 | |
---|
358 | (defun pg-goals-construct-command () |
---|
359 | ;; Examine the goals |
---|
360 | (let* ((span (span-at (point) 'goalsave)) ;; goalsave means subgoal no/name |
---|
361 | (top-span (span-at (point) 'proof-top-element)) |
---|
362 | top-info) |
---|
363 | (if (null top-span) () |
---|
364 | (setq top-info (span-property top-span 'proof-top-element)) |
---|
365 | (pop-to-buffer proof-script-buffer) |
---|
366 | (cond |
---|
367 | (span |
---|
368 | (proof-shell-invisible-command |
---|
369 | (format (if (eq 'hyp (car top-info)) pbp-hyp-command |
---|
370 | pbp-goal-command) |
---|
371 | (concat (cdr top-info) (proof-expand-path |
---|
372 | (span-property span 'goalsave)))))) |
---|
373 | ((eq (car top-info) 'hyp) |
---|
374 | ;; Switch focus to another subgoal; a non-scripting command |
---|
375 | (proof-shell-invisible-command |
---|
376 | (format pbp-hyp-command (cdr top-info)))) |
---|
377 | (t |
---|
378 | (proof-insert-pbp-command |
---|
379 | (format pg-goals-change-goal (cdr top-info)))))))) |
---|
380 | |
---|
381 | |
---|
382 | (defun pg-goals-get-subterm-help (spanorwin &optional obj pos) |
---|
383 | "Return a help string for subterm, called via 'help-echo property." |
---|
384 | (let ((span (or obj spanorwin))) ;; GNU Emacs vs XEmacs interface |
---|
385 | (if (and pg-subterm-help-cmd (span-live-p span)) |
---|
386 | (or (span-property span 'cachedhelp) ;; already got |
---|
387 | (progn |
---|
388 | (if (proof-shell-available-p) |
---|
389 | (let ((result |
---|
390 | (proof-shell-invisible-cmd-get-result |
---|
391 | (format pg-subterm-help-cmd (span-string span)) |
---|
392 | 'ignorerrors))) |
---|
393 | ;; FIXME: generalise, and make output readable |
---|
394 | ;; (fontify? does that work for GNU Emacs? |
---|
395 | ;; how can we do it away from a buffer?) |
---|
396 | (setq result |
---|
397 | (replace-in-string |
---|
398 | result |
---|
399 | (concat "\n\\|" pg-special-char-regexp) "")) |
---|
400 | (set-span-property span 'cachedhelp result) |
---|
401 | result))))))) |
---|
402 | |
---|
403 | |
---|
404 | |
---|
405 | (provide 'pg-goals) |
---|
406 | ;; pg-goals.el ends here. |
---|