1 | Index: generic/pg-vars.el |
---|
2 | =================================================================== |
---|
3 | RCS file: /disk/cvs/proofgen/ProofGeneral/generic/pg-vars.el,v |
---|
4 | retrieving revision 1.3 |
---|
5 | diff -c -r1.3 pg-vars.el |
---|
6 | *** generic/pg-vars.el 16 Jan 2008 21:43:48 -0000 1.3 |
---|
7 | --- generic/pg-vars.el 30 Jan 2008 13:45:15 -0000 |
---|
8 | *************** |
---|
9 | *** 131,136 **** |
---|
10 | --- 131,140 ---- |
---|
11 | Set to 'error or 'interrupt if one was observed from the proof |
---|
12 | assistant during the last group of commands.") |
---|
13 | |
---|
14 | + (defvar proof-shell-interrupt-pending nil |
---|
15 | + "Non-nil indicates that an interrupt is pending. |
---|
16 | + The queue will be terminated on the next call to the filter function.") |
---|
17 | + |
---|
18 | (defvar pg-response-next-error nil |
---|
19 | "Error counter in response buffer to count for next error message.") |
---|
20 | |
---|
21 | Index: generic/pg-user.el |
---|
22 | =================================================================== |
---|
23 | RCS file: /disk/cvs/proofgen/ProofGeneral/generic/pg-user.el,v |
---|
24 | retrieving revision 8.12 |
---|
25 | diff -c -r8.12 pg-user.el |
---|
26 | *** generic/pg-user.el 30 Jan 2008 13:37:45 -0000 8.12 |
---|
27 | --- generic/pg-user.el 30 Jan 2008 13:45:17 -0000 |
---|
28 | *************** |
---|
29 | *** 163,168 **** |
---|
30 | --- 163,169 ---- |
---|
31 | (with-current-buffer proof-shell-buffer |
---|
32 | ;; Send send an interrrupt, without comint-skip-input effect. |
---|
33 | ;; Interrupt is processed inside proof-shell. |
---|
34 | + (setq proof-shell-interrupt-pending t) |
---|
35 | (interrupt-process nil comint-ptyp) |
---|
36 | (run-hooks 'proof-shell-pre-interrupt-hook))) |
---|
37 | |
---|
38 | Index: generic/proof-shell.el |
---|
39 | =================================================================== |
---|
40 | RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-shell.el,v |
---|
41 | retrieving revision 8.44 |
---|
42 | diff -c -r8.44 proof-shell.el |
---|
43 | *** generic/proof-shell.el 30 Jan 2008 13:44:12 -0000 8.44 |
---|
44 | --- generic/proof-shell.el 30 Jan 2008 13:45:19 -0000 |
---|
45 | *************** |
---|
46 | *** 523,528 **** |
---|
47 | --- 523,529 ---- |
---|
48 | proof-shell-proof-completed nil |
---|
49 | proof-nesting-depth 0 |
---|
50 | proof-shell-error-or-interrupt-seen nil |
---|
51 | + proof-shell-interrupt-pending nil |
---|
52 | proof-shell-silent nil |
---|
53 | proof-shell-last-output nil |
---|
54 | proof-shell-last-output-kind nil |
---|
55 | *************** |
---|
56 | *** 710,715 **** |
---|
57 | --- 711,717 ---- |
---|
58 | (proof-warning |
---|
59 | "Interrupt: script management may be in an inconsistent state |
---|
60 | (but it's probably okay)")) |
---|
61 | + (setq proof-shell-interrupt-pending nil) |
---|
62 | (proof-shell-error-or-interrupt-action 'interrupt)) |
---|
63 | |
---|
64 | (defun proof-shell-error-or-interrupt-action (&optional err-or-int) |
---|
65 | *************** |
---|
66 | *** 1585,1591 **** |
---|
67 | (cond |
---|
68 | ((eq proof-shell-last-output-kind 'error) |
---|
69 | (proof-shell-handle-error cmd)) |
---|
70 | ! ((eq proof-shell-last-output-kind 'interrupt) |
---|
71 | (proof-shell-handle-interrupt)) |
---|
72 | ((eq proof-shell-last-output-kind 'loopback) |
---|
73 | (proof-shell-insert-loopback-cmd proof-shell-last-output) |
---|
74 | --- 1587,1594 ---- |
---|
75 | (cond |
---|
76 | ((eq proof-shell-last-output-kind 'error) |
---|
77 | (proof-shell-handle-error cmd)) |
---|
78 | ! ((or proof-shell-interrupt-pending |
---|
79 | ! (eq proof-shell-last-output-kind 'interrupt)) |
---|
80 | (proof-shell-handle-interrupt)) |
---|
81 | ((eq proof-shell-last-output-kind 'loopback) |
---|
82 | (proof-shell-insert-loopback-cmd proof-shell-last-output) |
---|