diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 17:06:02 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 17:06:02 +0000 |
| commit | 4565e25ab7be545bee7f39b84bf8368d80e17c85 (patch) | |
| tree | 7cec2b5dea8bd6a14ec546199805d74f496e741d | |
| parent | e7fc66ee95311cd7c2565dd1e76ce8d3fbb83baa (diff) | |
Tidy proof-interrupt-process
| -rw-r--r-- | generic/proof-script.el | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index b26e1d32..ae5cee1e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1408,15 +1408,11 @@ the proof script." (defun proof-interrupt-process () "Interrupt the proof assistant. Warning! This may confuse Proof General." (interactive) - (if (not (proof-shell-live-buffer)) + (unless (proof-shell-live-buffer) (error "Proof Process Not Started!")) - ; 1.10.99 da: removed this test, it seems silly. - ; (if (not (eq (current-buffer) proof-script-buffer)) - ; (error "Don't own process!")) - (if (not proof-shell-busy) - (error "Proof Process Not Active!")) - (save-excursion - (set-buffer proof-shell-buffer) + (unless proof-shell-busy + (error "Proof Process Not Active!")) + (with-current-buffer proof-shell-buffer (comint-interrupt-subjob))) |