diff options
| author | David Aspinall | 2008-01-29 23:08:52 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-01-29 23:08:52 +0000 |
| commit | 1350dafff63d381ba25b5b333d3637af2eeca4db (patch) | |
| tree | 6b97b277ab53b7d6e37cdcd413c6307c5fdc6be4 /generic | |
| parent | b15aac581cf3ab0abc1d7d732a6fab1e7a4e0623 (diff) | |
proof-interrupt-process: avoid effect of comint-skip-input (printing interrupt key).
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 80794058..a9807988 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -18,7 +18,7 @@ (require 'span) (require 'proof) ; loader (require 'proof-script) ; we build on proof-script -(require 'comint) ; comint-interrupt-subjob +(require 'comint) ; comint-interrupt-subjob/comint-ptyp (eval-when-compile (require 'completion)) ; loaded dynamically at runtime @@ -161,9 +161,9 @@ handling of interrupt signals." (unless proof-shell-busy (error "Proof Process Not Active!")) (with-current-buffer proof-shell-buffer - ;; Just send an interrrupt. - ;; Action on receiving one is triggered in proof-shell - (comint-interrupt-subjob) + ;; Send send an interrrupt, without comint-skip-input effect. + ;; Interrupt is processed inside proof-shell. + (interrupt-process nil comint-ptyp) (run-hooks 'proof-shell-pre-interrupt-hook))) |