Removed references of proof-shell-noise-regexp

5 files changed, 2 insertions, 12 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 85431e50..e31b0029 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -401,7 +401,6 @@
         proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp
         proof-shell-error-regexp coq-error-regexp
 	proof-shell-interrupt-regexp coq-interrupt-regexp
-        proof-shell-noise-regexp ""
         proof-shell-assumption-regexp coq-id
         proof-shell-goal-regexp coq-goal-regexp
         proof-shell-first-special-char ?\360
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 5a5bc089..d76b7fcc 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -851,10 +851,6 @@ assistant, for example, to switch to a new theory."
 Used by proof mode to parse proofstate output, and also
 to set outline heading regexp.")
 
-(defvar proof-shell-noise-regexp nil
-  "Unwanted information output from the proof process within
-  `proof-start-goals-regexp' and `proof-end-goals-regexp'.")
-
 (defvar proof-analyse-using-stack nil
   "Are annotations sent by proof assistant local or global")
 
diff --git a/isa/isa.el b/isa/isa.el
index 56f82a68..292f6095 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -157,9 +157,6 @@ no regular or easily discernable structure."
    
    ;; nothing appropriate for: proof-shell-abort-goal-regexp
 
-   ;; proof-shell-noise-regexp isn't used anywhere at the moment.
-   proof-shell-noise-regexp	        "val it = () : unit\n"
-
    ;; matches names of assumptions
    proof-shell-assumption-regexp	isa-id
    ;; matches subgoal name
diff --git a/lego/lego.el b/lego/lego.el
index 8821591a..4dcaa46c 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -454,7 +454,6 @@ We assume that module identifiers coincide with file names."
         proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp
         proof-shell-error-regexp lego-error-regexp
 	proof-shell-interrupt-regexp lego-interrupt-regexp
-        proof-shell-noise-regexp "Discharge\\.\\. "
         proof-shell-assumption-regexp lego-id
         proof-shell-goal-regexp lego-goal-regexp
         proof-shell-first-special-char ?\360
diff --git a/todo b/todo
index c7b55385..8638131c 100644
--- a/todo
+++ b/todo
@@ -87,9 +87,8 @@ B da: goal-hyp: this should be more generic.  At the moment, there are
   default behaviour for proof-goal-hyp-fn a hook function.
   That will work for Isabelle too.   (15 mins)
 
-B proof-shell-noise-regexp: seems unused at present, but set
-  in the specific directories.  Either use it or be rid of it!
-  (tms, apparently is used in LEGO mode but should be generic?)
+D Add support to filter out unwanted noise from the prover by setting
+  up a regular expression  proof-shell-noise-regexp (1h)
 
 A Check that byte compilation (and compiled code!) 
   works for both varieties of Emacs.