Important regular expression fixes:

 -error-regexp		   doesn't match warnings now.
 -annotated-prompt-regexp  doesn't match warnings now,
			   and is different from -prompt-regexp.

3 files changed, 27 insertions, 24 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 100aa4ad..c47d11c4 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -30,11 +30,14 @@ in
 
 (*hooks for output channels: normal, warning, error*)
 
-(* da: NO CHANGES NEEDED YET *)
+(* Proof General: no change to these yet from defaults, but be
+   careful that proof-shell-prompt-pattern doesn't match any
+   of these!  (maybe the default needs adjustment)
+*)
 val () =
 	(prs_fn := (fn s => out s);
 	 warning_fn := (fn s => out (prefix_lines "### " s));
-	error_fn := (fn s => out (prefix_lines "*** " s)))
+	 error_fn := (fn s => out (prefix_lines "*** " s)))
 
 end;
 
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 33e73d41..886a686b 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -100,13 +100,6 @@
 
 ;; ----- regular expressions
 
-;; this should come from isa-ml-compiler stuff.
-(defcustom isa-error-regexp 
-  "^.*Error:\\|^\\*\\*\\*"
-  "A regexp indicating that Isabelle has identified an error."
-  :type 'string
-  :group 'isa-syntax)
-
 (defconst isa-id proof-id)
 
 (defconst isa-ids (proof-ids isa-id))
diff --git a/isa/isa.el b/isa/isa.el
index 361a87aa..8fa15a2f 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -82,25 +82,32 @@ no regular or easily discernable structure."
 (defun isa-shell-mode-config-set-variables ()
   "Configure generic proof shell mode variables for Isabelle."
   (setq
-   proof-shell-prompt-pattern
-   "^\\(val it = () : unit\n\\)?2?[-=#>]>? *"
-   ;"^[-=#>]>? *"
-   ;; This pattern matches a variety of prompts from ML.
-   ;; It doesn't match the tracing output prompt.
+   ;; This first pattern is crucial.
+   ;; It should match the 'top-level' prompt from ML,
+   ;; optionally proceeded by vacuous assignment output.
+   ;;
+   ;; It doesn't match the tracing output prompt or secondary
+   ;; prompts (continued lines), although these would usually
+   ;; be nice for comint-prompt-regexp to work.
+   ;; 
    ;; Probably it isn't general enough for all MLs, please send me
    ;; problem reports / patches.
-   ;; Alternative version to match vacuous assignments:
-     
-   ;; this doesn't work as intended, probably because the
-   ;; process mungling searches backwards and forwards for
-   ;; regexps.
+   ;;
+   proof-shell-annotated-prompt-pattern
+			          "^\\(val it = () : unit\n\\)?> "
+
+   ;; This pattern is just for comint, it matches a range of
+   ;; prompts from a range of MLs.
+   proof-shell-prompt-pattern     "^2?[-=#>]>? *"
+
    proof-shell-cd			"cd \"%s\";"
-   ;; this one not set: proof-shell-abort-goal-regexp 
    proof-shell-proof-completed-regexp   "No subgoals!"
-   proof-shell-error-regexp		isa-error-regexp
-   proof-shell-interrupt-regexp         "Interrupt"     ; FIXME: only good for NJ/SML
+   ;; FIXME: the next two are probably only good for NJ/SML
+   proof-shell-error-regexp		"^.*Error:\\|^\\*\\*\\*"
+   proof-shell-interrupt-regexp         "Interrupt"
+   ;; this one not set: proof-shell-abort-goal-regexp 
    proof-shell-noise-regexp	        ""
-   proof-shell-assumption-regexp	isa-id		   ; matches name of assumptions
+   proof-shell-assumption-regexp	isa-id  ; matches name of assumptions
    proof-shell-goal-regexp		isa-goal-regexp    ; matches subgoal heading
    ;; We can't hack the SML prompt, so set wakeup-char to nil.
    proof-shell-wakeup-char		nil
@@ -113,7 +120,7 @@ no regular or easily discernable structure."
 					 "use \""
 					 proof-internal-home-directory
 					  "isa/ProofGeneral.ML\";")
-   proof-shell-eager-annotation-start   "^\\[opening "
+   proof-shell-eager-annotation-start   "^\\[opening \\|^###"
   ;;   proof-shell-eager-annotation-end "$"
    proof-shell-eager-annotation-end     "$"
    ;; === ANNOTATIONS  === ones below here are broken