Ticket #179: local-interrupt.patch

File local-interrupt.patch, 3.0 KB (added by David Aspinall, 12 years ago)

Add a route for the code to signal interrupt to itself, without relying on an interrupt message in the proof shell.

Line 
1Index: generic/pg-vars.el
2===================================================================
3RCS file: /disk/cvs/proofgen/ProofGeneral/generic/pg-vars.el,v
4retrieving revision 1.3
5diff -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 
21Index: generic/pg-user.el
22===================================================================
23RCS file: /disk/cvs/proofgen/ProofGeneral/generic/pg-user.el,v
24retrieving revision 8.12
25diff -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   
38Index: generic/proof-shell.el
39===================================================================
40RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-shell.el,v
41retrieving revision 8.44
42diff -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)