From 4565e25ab7be545bee7f39b84bf8368d80e17c85 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 6 Oct 1999 17:06:02 +0000 Subject: Tidy proof-interrupt-process --- generic/proof-script.el | 12 ++++-------- 1 file 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))) -- cgit v1.2.3