From aff2ea4bbb63aff1a85b759e5541e3b7683d9776 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 8 Sep 2009 21:02:28 +0000
Subject: Remove barely useful proof-shell-abort-goal-regexp (only served to
 sanitize LEGO messages)

---
 generic/proof-config.el | 5 -----
 isar/isar.el            | 1 -
 lego/lego.el            | 6 ------
 plastic/plastic.el      | 5 -----
 4 files changed, 17 deletions(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 83c0c4f7..a4b9bb0f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1091,11 +1091,6 @@ in ordinary output, which should appear in this regexp."
   :type 'regexp
   :group 'proof-shell)
 
-(defcustom proof-shell-abort-goal-regexp nil
-  "Regexp matching output from an aborted proof."
-  :type 'regexp
-  :group 'proof-shell)
-
 (defcustom proof-shell-error-regexp nil
   "Regexp matching an error report from the proof assistant.
 
diff --git a/isar/isar.el b/isar/isar.el
index a1ca86a1..19abfedc 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -183,7 +183,6 @@ See -k option for Isabelle interface script."
    proof-shell-interrupt-regexp         "\^AM\\*\\*\\* Interrupt"
    proof-shell-error-regexp             "\^AM\\*\\*\\*"
    proof-shell-proof-completed-regexp   nil     ; n.a.
-   proof-shell-abort-goal-regexp        nil     ; n.a.
 
    pg-next-error-regexp	  "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)"
    pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)"
diff --git a/lego/lego.el b/lego/lego.el
index 73552f20..be48be41 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -104,11 +104,6 @@ Activates extended printing routines required for Proof General.")
 (defvar lego-shell-cd "Cd \"%s\";"
   "*Command of the inferior process to change the directory.")
 
-(defvar lego-shell-abort-goal-regexp
-  "KillRef: ok, not in proof state\\|Forget forced KillRef"
-  "*Regular expression indicating that the proof of the current goal
-  has been abandoned.")
-
 (defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*"
   "*Regular expression indicating that the proof has been completed.")
 
@@ -380,7 +375,6 @@ For LEGO, we assume that module identifiers coincide with file names."
 
 (defun lego-shell-mode-config ()
   (setq proof-shell-cd-cmd lego-shell-cd
-	proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp
 	proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp
 	proof-shell-error-regexp lego-error-regexp
 	proof-shell-interrupt-regexp lego-interrupt-regexp
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 5a7a7f03..2fceda64 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -125,10 +125,6 @@
   (concat plastic-lit-string " &S ECHO no cd ;\n")
   "*Command of the inferior process to change the directory.")
 
-(defvar plastic-shell-abort-goal-regexp "KillRef: ok, not in proof state"
-  "*Regular expression indicating that the proof of the current goal
-  has been abandoned.")
-
 (defvar plastic-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*"
   "*Regular expression indicating that the proof has been completed.")
 
@@ -451,7 +447,6 @@ For Plastic, we assume that module identifiers coincide with file names."
 
 (defun plastic-shell-mode-config ()
   (setq proof-shell-cd-cmd plastic-shell-cd
-	proof-shell-abort-goal-regexp plastic-shell-abort-goal-regexp
 	proof-shell-proof-completed-regexp plastic-shell-proof-completed-regexp
 	proof-shell-error-regexp plastic-error-regexp
 	proof-shell-interrupt-regexp plastic-interrupt-regexp
-- 
cgit v1.2.3