blob: 519df70836df8747c61d2dd72f82d5a9fe0204e3 (
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
|
Patch below doesn't work because it examines the head of the
proof-action-list which is empty by the time
proof-handle-delayed-output gets called!
Best thing may be to temporarily extend
proof-handle-delayed-output-hook with a function to clear the erase
flag... BUT can't remove it from proof-shell-done-invisible,
because that's too early!!! Argh.
Maybe we need a special test in the exec loop for just one element in
the action list, and then call the callback *after* handling delayed
output?
Um. Not for 3.0, then.
*** ProofGeneral.prev/generic/proof-shell.el Thu Nov 18 13:07:33 1999
--- ProofGeneral/generic/proof-shell.el Thu Nov 18 13:03:25 1999
***************
*** 676,682 ****
;; Erase the response buffer if need be, maybe also removing the
;; window. Indicate that it should be erased before the next
;; output.
! (proof-shell-maybe-erase-response t t)
(set-buffer proof-goals-buffer)
--- 676,684 ----
;; Erase the response buffer if need be, maybe also removing the
;; window. Indicate that it should be erased before the next
;; output.
! (proof-shell-maybe-erase-response
! (or proof-shell-erase-response-flag t) ; preserve invisible cmd o/p
! t)
(set-buffer proof-goals-buffer)
***************
*** 829,835 ****
(unless proof-shell-leave-annotations-in-output
(setq str (proof-shell-strip-special-annotations str)))
! (proof-shell-maybe-erase-response t nil)
(proof-response-buffer-display str)
(proof-display-and-keep-buffer proof-response-buffer))
;;
--- 831,847 ----
(unless proof-shell-leave-annotations-in-output
(setq str (proof-shell-strip-special-annotations str)))
! (proof-shell-maybe-erase-response
! ;; Magical detection of invisible commands, whose output
! ;; gets preserved specially.
! (if (and
! (not (eq proof-shell-erase-response-flag 'invisible))
! (eq (nth 2 (car-safe proof-action-list))
! 'proof-shell-done-invisible))
! 'invisible
! t) ; erase next time, probably
! t) ; clean.
!
(proof-response-buffer-display str)
(proof-display-and-keep-buffer proof-response-buffer))
;;
|
