Fixed coalescing of error messages: all error messages from

the last command are now show. Added extra docs to clarify behaviour.

3 files changed, 19 insertions, 8 deletions

diff --git a/CHANGES b/CHANGES
index 4a5ee759..d5e9787d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -85,6 +85,10 @@ Isabelle and Isar Changes
   are now closed off automatically when a new goal is begun,
   mirroring the behaviour of Isabelle.
 
+* Confusing display of only last error is fixed: multiple
+  error messages are now coalesced properly.
+
+
 
 Only in the developers' release
 -------------------------------
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 77667b61..c52421ae 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -922,6 +922,9 @@ this regexp.  Moreover, an error message should not be matched as an
 eager annotation (see proof-shell-eager-annotation-start) otherwise it
 will be lost.
 
+Error messages are considered to begin from proof-shell-error-regexp
+and continue until the next prompt.
+
 The engine matches interrupts before errors, see proof-shell-interupt-regexp.
 
 It is safe to leave this variable unset (as nil)."
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index ccb8515d..dd04b3ee 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -725,17 +725,21 @@ This is a list of tuples of the form (TYPE . STRING). type is either
 
 (defun proof-shell-handle-output (start-regexp end-regexp append-face)
   "Displays output from `proof-shell-buffer' in `proof-response-buffer'.
-The region in `proof-shell-buffer begins with the match for START-REGEXP
-and is delimited by END-REGEXP. The match for END-REGEXP is not
-part of the specified region.
+The region in `proof-shell-buffer begins with the first match 
+beyond the prompt for START-REGEXP and is delimited by the
+last match in the buffer for END-REGEXP.  The match for END-REGEXP 
+is not part of the specified region.  This mechanism means if there
+are multiple matches for START-REGEXP and END-REGEXP, we match the
+largest region containing them all.
 Returns the string (with faces) in the specified region."
   (let (start end string)
     (save-excursion
       (set-buffer proof-shell-buffer)
       (goto-char (point-max))
-      (setq start (search-backward-regexp start-regexp))
-      (setq end (- (search-forward-regexp end-regexp)
-				   (length (match-string 0))))
+      (setq end (search-backward-regexp end-regexp))
+      (goto-char (marker-position proof-marker))
+      (setq start (- (search-forward-regexp start-regexp)
+		     (length (match-string 0))))
       (setq string
 	    (if proof-shell-leave-annotations-in-output
 		(buffer-substring start end)
@@ -847,7 +851,7 @@ Then we call `proof-shell-handle-error-hook'. "
     ;; Alternatively one could higlight all output between the
     ;; previous and the current prompt.
     ;; +/- of our approach
-    ;; + Previous not so relevent output is not highlighted
+    ;; + Previous not so relevant output is not highlighted
     ;; - Proof systems have to conform to error messages whose start can be
     ;;   detected by a regular expression.
   (proof-shell-handle-output
@@ -1116,7 +1120,7 @@ The return value is non-nil if the action list is now empty."
 		     (proof-detach-queue)
 		     ;; indicate finished
 		     t)
-	    ;; Send the next command to the process
+	    ;; Otherwise send the next command to the process
 	    (proof-shell-insert (nth 1 item))
 	    ;; indicate not finished
 	    nil)))))