From bc8a80167ad13742d4cf6b6bf794883516429517 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Wed, 7 Dec 2011 09:23:09 +0000
Subject: - 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

---
 coq/coq.el | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

(limited to 'coq')

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: 
-- 
cgit v1.2.3