diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | coq/coq.el | 36 | ||||
| -rw-r--r-- | generic/proof-shell.el | 4 |
3 files changed, 39 insertions, 3 deletions
@@ -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 @@ -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))) |