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
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Displaying in the response buffer
;;
;; Flag and function to keep response buffer tidy.
(defvar pg-response-erase-flag nil
"Indicates that the response buffer should be cleared before next message.")
(defun proof-shell-maybe-erase-response
(&optional erase-next-time clean-windows force)
"Erase the response buffer according to pg-response-erase-flag.
ERASE-NEXT-TIME is the new value for the flag.
If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing.
If FORCE, override pg-response-erase-flag.
If the user option proof-tidy-response is nil, then
the buffer is only cleared when FORCE is set.
No effect if there is no response buffer currently.
Returns non-nil if response buffer was cleared."
(when (buffer-live-p proof-response-buffer)
(let ((doit (or (and
proof-tidy-response
(not (eq pg-response-erase-flag 'invisible))
pg-response-erase-flag)
force)))
(if doit
(if clean-windows
(proof-clean-buffer proof-response-buffer)
;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
;; (erase-buffer proof-response-buffer)
(with-current-buffer proof-response-buffer
(setq pg-response-next-error nil) ; all error msgs lost!
(erase-buffer)
(set-buffer-modified-p nil))))
(setq pg-response-erase-flag erase-next-time)
doit)))
(defun pg-response-display (str)
"Show STR as a response in the response buffer."
(unless pg-use-specials-for-fontify
(setq str (pg-assoc-strip-subterm-markup str)))
;;HERE changed t nil to t FORCE
(proof-shell-maybe-erase-response t nil)
;;(unless (or (string-equal str "") (string-equal str "\n"))
;; don't display an empty buffer [ NB: above test repeated below,
;; but response-display reused elsewhere ]
(pg-response-display-with-face str)
;; NB: this displays an empty buffer sometimes when it's not
;; so useful. It _is_ useful if the user has requested to
;; see the proof state and there is none
;; (Isabelle/Isar displays nothing: might be better if it did).
(proof-display-and-keep-buffer proof-response-buffer))
;; FIXME: this function should be combined with
;; proof-shell-maybe-erase-response-buffer.
(defun pg-response-display-with-face (str &optional face)
"Display STR with FACE in response buffer."
;; 3.4: no longer return fontified STR, it wasn't used.
(cond
((string-equal str ""))
((string-equal str "\n")) ; quick exit, no display.
(t
(let (start end)
(with-current-buffer proof-response-buffer
;; da: I've moved newline before the string itself, to match
;; the other cases when messages are inserted and to cope
;; with warnings after delayed output (non newline terminated).
(goto-char (point-max))
;; insert a newline before the new message unless the
;; buffer is empty
(unless (eq (point-min) (point-max))
(newline))
(setq start (point))
(insert str)
(unless (bolp) (newline))
(proof-fontify-region start (point))
;; This is one reason why we don't keep the buffer in font-lock
;; minor mode: it destroys this hacky property as soon as it's
;; made! (Using the minor mode is much more convenient, tho')
(if (and face proof-output-fontify-enable)
(font-lock-append-text-property
start (point-max) 'face face))
;; This returns the decorated string, but it doesn't appear
;; decorated in the minibuffer, unfortunately.
;; [ FIXME: users have asked for that to be fixed ]
;; 3.4: remove this for efficiency.
;; (buffer-substring start (point-max))
(set-buffer-modified-p nil))))))
(defun pg-response-clear-displays ()
"Clear Proof General response buffers.
You can use this command to clear the output from these buffers when
it becomes overly long. Particularly useful when `proof-tidy-response'
is set to nil, so responses are not cleared automatically."
(interactive)
(proof-map-buffers (list proof-response-buffer proof-trace-buffer proof-resolve-buffer)
(erase-buffer)
(set-buffer-modified-p nil)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Displaying in the resolution buffer
;;
;; Flag and function to keep resolve buffer tidy.
(defvar pg-resolve-erase-flag nil
"Indicates that the resolve buffer should be cleared before next message.")
(defun proof-shell-maybe-erase-resolve
(&optional erase-next-time clean-windows force)
"Erase the resolve buffer according to pg-resolve-erase-flag.
ERASE-NEXT-TIME is the new value for the flag.
If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing.
If FORCE, override pg-resolve-erase-flag.
If the user option proof-tidy-resolve is nil, then
the buffer is only cleared when FORCE is set.
No effect if there is no resolve buffer currently.
Returns non-nil if resolve buffer was cleared."
(when (buffer-live-p proof-resolve-buffer)
(let ((doit (or (and
proof-tidy-resolve
(not (eq pg-resolve-erase-flag 'invisible))
pg-resolve-erase-flag)
force)))
(if doit
(if clean-windows
(proof-clean-buffer proof-resolve-buffer)
;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
;; (erase-buffer proof-resolve-buffer)
(with-current-buffer proof-resolve-buffer
(setq pg-resolve-next-error nil) ; all error msgs lost!
(erase-buffer)
(set-buffer-modified-p nil))))
(setq pg-resolve-erase-flag erase-next-time)
doit)))
(defun pg-resolve-display (str)
"Show STR as a resolve in the resolve buffer."
(unless pg-use-specials-for-fontify
(setq str (pg-assoc-strip-subterm-markup str)))
(proof-shell-maybe-erase-resolve t nil)
;;(unless (or (string-equal str "") (string-equal str "\n"))
;; don't display an empty buffer [ NB: above test repeated below,
;; but resolve-display reused elsewhere ]
(pg-resolve-display-with-face str)
;; NB: this displays an empty buffer sometimes when it's not
;; so useful. It _is_ useful if the user has requested to
;; see the proof state and there is none
;; (Isabelle/Isar displays nothing: might be better if it did).
(proof-display-and-keep-buffer proof-resolve-buffer))
;; FIXME: this function should be combined with
;; proof-shell-maybe-erase-resolve-buffer.
(defun pg-resolve-display-with-face (str &optional face)
"Display STR with FACE in resolve buffer."
;; 3.4: no longer return fontified STR, it wasn't used.
(cond
((string-equal str ""))
((string-equal str "\n")) ; quick exit, no display.
(t
(let (start end)
(with-current-buffer proof-resolve-buffer
;; da: I've moved newline before the string itself, to match
;; the other cases when messages are inserted and to cope
;; with warnings after delayed output (non newline terminated).
(goto-char (point-max))
;; insert a newline before the new message unless the
;; buffer is empty
(unless (eq (point-min) (point-max))
(newline))
(setq start (point))
(insert str)
(unless (bolp) (newline))
(proof-fontify-region start (point))
;; This is one reason why we don't keep the buffer in font-lock
;; minor mode: it destroys this hacky property as soon as it's
;; made! (Using the minor mode is much more convenient, tho')
(if (and face proof-output-fontify-enable)
(font-lock-append-text-property
start (point-max) 'face face))
;; This returns the decorated string, but it doesn't appear
;; decorated in the minibuffer, unfortunately.
;; [ FIXME: users have asked for that to be fixed ]
;; 3.4: remove this for efficiency.
;; (buffer-substring start (point-max))
(set-buffer-modified-p nil))))))
(defun pg-resolve-clear-displays ()
"Clear Proof General resolve buffer.
You can use this command to clear the output from these buffers when
it becomes overly long. Particularly useful when `proof-tidy-resolve'
is set to nil, so resolves are not cleared automatically."
(interactive)
(proof-map-buffers (list proof-resolve-buffer proof-trace-buffer proof-resolve-buffer)
(erase-buffer)
(set-buffer-modified-p nil)))
|
