- protect proof-shell-handle-delayed-output against the case where

  proof-shell-end-goals-regexp is defined but does not match
- add coq setting for hiding additional subgoals

3 files changed, 39 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 2a61b8b4..0762a7e5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
 
 *** Minor parsing fixes
 
+*** New setting for hiding additional goals from the *goals* buffer
+
 
 * Changes of Proof General 4.1 from Proof General 4.0
 
diff --git a/coq/coq.el b/coq/coq.el
index 6bf7527e..bcebe90f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -27,6 +27,7 @@
   (defvar coq-use-editing-holes nil)    ; defpacustom
   (defvar coq-compile-before-require nil)       ; defpacustom
   (defvar coq-confirm-external-compilation nil) ; defpacustom
+  (defvar coq-hide-additional-subgoals nil) ; defpacustom
   (proof-ready-for-assistant 'coq))     ; compile for coq
 
 (require 'proof)
@@ -174,6 +175,19 @@ On Windows you might need something like:
   :type 'string
   :group 'coq)
 
+(defcustom coq-end-goals-regexp-hide-subgoals "\nsubgoal 2 is:"
+  "Regexp for `proof-shell-end-goals-regexp' when hiding additional subgoals.
+See also `coq-hide-additional-subgoals'."
+  :type '(choice regexp (const nil))
+  :group 'coq)
+
+(defcustom coq-end-goals-regexp-show-subgoals nil
+  "Regexp for `proof-shell-end-goals-regexp' when showing all subgoals.
+A setting of nil means show all output from Coq. See also
+`coq-hide-additional-subgoals'."
+  :type '(choice regexp (const nil))
+  :group 'coq)
+
 
 ;;
 ;; Outline mode
@@ -846,6 +860,15 @@ If locked span already has a state number, then do nothing. Also updates
   ;;   t))))
 
 
+(defun coq-hide-additional-subgoals-switch ()
+  "Function invoked when the user switches `coq-hide-additional-subgoals'."
+  (message "chass")
+  (if coq-hide-additional-subgoals
+      (setq proof-shell-end-goals-regexp coq-end-goals-regexp-hide-subgoals)
+    (setq proof-shell-end-goals-regexp coq-end-goals-regexp-show-subgoals)))
+    
+
+
 ;;
 ;; Commands for Coq
 ;;
@@ -1182,7 +1205,11 @@ This is specific to `coq-mode'."
    proof-shell-result-end "\372 End Pbp result \373"
 
    proof-shell-start-goals-regexp          "^[0-9]+ subgoals?"
-   proof-shell-end-goals-regexp nil        ; up to next prompt
+   proof-shell-end-goals-regexp
+   (if coq-hide-additional-subgoals
+       (setq proof-shell-end-goals-regexp coq-end-goals-regexp-hide-subgoals)
+     (setq proof-shell-end-goals-regexp coq-end-goals-regexp-show-subgoals))
+
    proof-shell-init-cmd coq-shell-init-cmd
 
    proof-no-fully-processed-buffer t
@@ -1228,6 +1255,13 @@ This is specific to `coq-mode'."
 ;;  :setting ("Focus. " . "Unfocus. "))
 
 
+(defpacustom hide-additional-subgoals nil
+  "Only show the current goal, hiding additional subgoals."
+  :type 'boolean
+  :safe 'booleanp
+  :eval (coq-hide-additional-subgoals-switch))
+
+
 ;; FIXME: to handle "printing all" properly, we should change the state
 ;; of the variables that also depend on it.
 ;; da: 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 6abef30b..a2402013 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1502,9 +1502,9 @@ i.e., 'goals or 'response."
        (while (re-search-forward proof-shell-start-goals-regexp end t)
 	 (setq gstart (match-beginning 0))
 	 (setq gend
-	       (if proof-shell-end-goals-regexp
+	       (if (and proof-shell-end-goals-regexp
+			(re-search-forward proof-shell-end-goals-regexp end t))
 		   (progn
-		     (re-search-forward proof-shell-end-goals-regexp end t)
 		     (setq rstart (match-end 0))
 		     (match-beginning 0))
 		 end)))