From c8cd8ace98d6e0f3ebdce7718d92229f0c31dbec Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 17 Aug 2009 16:45:41 +0000
Subject: Move proof-interrupt-process to proof-shell.  Add pending interrupt
 behaviour.  See http://proofgeneral.inf.ed.ac.uk/trac/ticket/179

---
 generic/pg-user.el | 27 ---------------------------
 1 file changed, 27 deletions(-)

(limited to 'generic/pg-user.el')

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 41fa4de9..642387c7 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -134,33 +134,6 @@ the proof script."
 	   (proof-maybe-follow-locked-end))
        (error "Not proving")))))
 
-;;
-;; Interrupt
-;;
-
-;;;###autoload
-(defun proof-interrupt-process ()
-  "Interrupt the proof assistant.  Warning! This may confuse Proof General.
-This sends an interrupt signal to the proof assistant, if Proof General
-thinks it is busy.
-
-This command is risky because when an interrupt is trapped in the
-proof assistant, we don't know whether the last command succeeded or
-not.  The assumption is that it didn't, which should be true most of
-the time, and all of the time if the proof assistant has a careful
-handling of interrupt signals."
-  (interactive)
-  (unless (proof-shell-live-buffer)
-      (error "Proof Process Not Started!"))
-  (unless proof-shell-busy
-    (error "Proof Process Not Active!"))
-  (with-current-buffer proof-shell-buffer
-    ;; 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)))
-  
-
 ;;
 ;; Movement commands
 ;;
-- 
cgit v1.2.3