Fixed up proof-shell-proof-completed mess nicely.

2 files changed, 1 insertions, 17 deletions

diff --git a/isa/BUGS b/isa/BUGS
index 0ec5719a..a6a3eec2 100644
--- a/isa/BUGS
+++ b/isa/BUGS
@@ -5,13 +5,6 @@
 See also ../BUGS for generic bugs.
 
 
-** "Stack overflow in regexp".  
-
-This problem is caused by a poor regexp and large proofstates.  It
-needs some small alterations to other proof assistant regexps, so will
-be fixed in 3.2.  In the meantime, a workaround is to reduce the
-number of subgoals displayed.
-
 ** set proof_timing is problematic
 
 It will make the goals display disappear during proof.  This is
diff --git a/isa/isa.el b/isa/isa.el
index acbb2b75..35eadc18 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -190,14 +190,7 @@ and script mode."
    proof-shell-end-goals-regexp		"\367"
    proof-shell-goal-char	        ?\370
 
-   ;; FIXME da: this needs improvement.  I don't know why just
-   ;; "No subgoals!" isn't enough.  (Maybe anchored to end-goals
-   ;; for safety).  At the moment, this regexp reportedly causes
-   ;; overflows with large proof states. 
-   proof-shell-proof-completed-regexp
-   (concat proof-shell-start-goals-regexp
-	   "\\(\\(.\\|\n\\)*\nNo subgoals!\n\\)"
-	   proof-shell-end-goals-regexp)
+   proof-shell-proof-completed-regexp	"^No subgoals!"
 
    ;; initial command configures Isabelle by hacking print functions.
    ;; FIXME: temporary hack for almost enabling/disabling printing.
@@ -217,8 +210,6 @@ and script mode."
    ;; annotations, see isa-output-font-lock-keywords-1
    proof-shell-leave-annotations-in-output t
 
-   proof-goals-display-qed-message	t
-
    ;; === ANNOTATIONS  === ones here are broken
    proof-shell-result-start	        "\372 Pbp result \373"
    proof-shell-result-end		"\372 End Pbp result \373"