Improve configuration for HOL Light. Allow goals display to be prefixed by ignored junk (val it : goalstack =).

2 files changed, 16 insertions, 7 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 83528b9f..f0633e72 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1155,7 +1155,11 @@ is shown to the user.  Set to nil to disable."
 This is an important setting.  Output between `proof-shell-start-goals-regexp'
 and `proof-shell-end-goals-regexp' will be pasted into the goals buffer
 and possibly analysed further for proof-by-pointing markup.
-If it is left as nil, the goals buffer will not be used."
+If it is left as nil, the goals buffer will not be used.
+
+The goals display starts at the beginning of the match on this
+regexp, unless it has a match group, in which case it starts
+at (match-end 1)."
   :type '(choice (const nil) regexp)
   :group 'proof-shell)
 
@@ -1165,10 +1169,10 @@ This allows a shorter form of the proof state output to be displayed,
 in case several messages are combined in a command output.
 
 The portion treated as the goals output will be that between the
-start of the match on `proof-shell-start-goals-regexp' and the
+match on `proof-shell-start-goals-regexp' (which see) and the
 start of the match on `proof-shell-end-goals-regexp'.
 
-If nil, use the whole of the output after
+If nil, use the whole of the output from the match on
 `proof-shell-start-goals-regexp' up to the next prompt."
   :type '(choice (const nil) regexp)
   :group 'proof-shell)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index ab0d2d05..9cdce998 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1518,11 +1518,16 @@ i.e., 'goals or 'response."
   (cond
    ((and proof-shell-start-goals-regexp
 	 (proof-re-search-forward proof-shell-start-goals-regexp end t))
-     (let* ((gstart (match-beginning 0))  (rstart start) gend)
+     (let* ((gmark  (match-beginning 0)) ; start of goals message
+	    (gstart (or (match-end 1)    ; start of actual display
+			gmark))
+	    (rstart start)		 ; possible response before goals
+	    (gend   end))
        ;; Find the last goal string in the output
        (goto-char gstart)
        (while (re-search-forward proof-shell-start-goals-regexp end t)
-	 (setq gstart (match-beginning 0))
+	 (setq gmark (match-beginning 0))
+	 (setq gstart (or (match-end 1) gmark))
 	 (setq gend
 	       (if (and proof-shell-end-goals-regexp
 			(re-search-forward proof-shell-end-goals-regexp end t))
@@ -1536,10 +1541,10 @@ i.e., 'goals or 'response."
 	 (pg-goals-display proof-shell-last-goals-output))
        ;; also allow (for Coq) any preceding output as a response
        ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp
-       (when (> (- gstart rstart) 4)
+       (when (> (- gmark rstart) 4)
 	 (proof-shell-display-output-as-response
 	  flags
-	  (buffer-substring-no-properties rstart gstart)))
+	  (buffer-substring-no-properties rstart gmark)))
        ;; primary output kind is goals
        'goals))