blob: a0b125a4123c4968e03c7725c593b9e60fd2103c (
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
|
;; pg-goals.el --- Proof General goals buffer mode.
;;
;; Copyright (C) 1994-2009 LFCS, University of Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;; Commentary:
;;; Code:
(eval-when-compile
(require 'easymenu) ; easy-menu-add, etc
(require 'cl) ; incf
(require 'span)) ; span-*
(require 'proof-utils)
(require 'pg-assoc)
(require 'bufhist)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Goals buffer mode
;;
;;;###autload
(define-derived-mode proof-goals-mode proof-universal-keys-only-mode
proof-general-name
"Mode for goals display.
May enable proof-by-pointing or similar features.
\\{proof-goals-mode-map}"
(setq proof-buffer-type 'goals)
(add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
(easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
(easy-menu-add proof-assistant-menu proof-goals-mode-map)
(proof-toolbar-setup)
(erase-buffer)
(buffer-disable-undo)
(if proof-keep-response-history (bufhist-mode)) ; history for contents
(set-buffer-modified-p nil)
(setq cursor-type 'bar))
;;
;; Menu for goals buffer
;;
(proof-eval-when-ready-for-assistant ; proof-aux-menu depends on <PA>
(easy-menu-define proof-goals-mode-menu
proof-goals-mode-map
"Menu for Proof General goals buffer."
(proof-aux-menu)))
;;
;; Keys for goals buffer
;;
(define-key proof-goals-mode-map [q] 'bury-buffer)
;; TODO: use standard Emacs button behaviour here (cf Info mode)
(define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
(define-key proof-goals-mode-map [C-mouse-3]
'proof-undo-and-delete-last-successful-command)
;;
;; The completion of init
;;
;;;###autoload
(defun proof-goals-config-done ()
"Initialise the goals buffer after the child has been configured."
(setq font-lock-defaults '(proof-goals-font-lock-keywords)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Goals buffer processing
;;
(defun pg-goals-display (string)
"Display STRING in the `proof-goals-buffer', properly marked up.
Converts term substructure markup into mouse-highlighted extents."
(save-excursion
;; Response buffer may be out of date. It may contain (error)
;; messages relating to earlier proof states
;; NB: this isn't always the case. In Isabelle
;; we get <WARNING MESSAGE> <CURRENT GOALS> output,
;; or <WARNING MESSAGE> <ORDINARY MESSAGE>. Both times
;; <WARNING MESSAGE> would be relevant.
;; We should only clear the output that was displayed from
;; the *previous* prompt.
;; Erase the response buffer if need be, maybe removing the
;; window. Indicate it should be erased before the next output.
(pg-response-maybe-erase t t)
;; Erase the goals buffer and add in the new string
(set-buffer proof-goals-buffer)
(unless (eq 0 (buffer-size))
(bufhist-checkpoint-and-erase))
;; Only display if string is non-empty.
(unless (string-equal string "")
(setq buffer-read-only nil)
(insert string)
(setq buffer-read-only t)
(set-buffer-modified-p nil)
;; Keep point at the start of the buffer.
(proof-display-and-keep-buffer
proof-goals-buffer (point-min)))))
;;
;; Actions in the goals buffer
;;
(defun pg-goals-button-action (event)
"Construct a command based on the mouse-click EVENT."
(interactive "e")
(let* ((posn (event-start event))
(pos (posn-point posn))
(buf (window-buffer (posn-window posn)))
(props (text-properties-at pos buf))
(sendback (plist-get props 'sendback)))
(cond
(sendback
(with-current-buffer buf
(let* ((cmdstart (previous-single-property-change pos 'sendback
nil (point-min)))
(cmdend (next-single-property-change pos 'sendback
nil (point-max)))
(cmd (buffer-substring-no-properties cmdstart cmdend)))
(proof-insert-sendback-command cmd)))))))
(provide 'pg-goals)
;;; pg-goals.el ends here
|
