From c7059c8f4e880f2b7f1ee895e0d4d32eee2f36fd Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 13 Jun 2018 11:08:05 +0200 Subject: Fix the fix #355. The fix was bad: no ore hyps were foldable/highlightable. --- coq/coq-syntax.el | 13 +++++++++++-- coq/coq.el | 8 ++++---- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 4bc8d984..5b12bd8e 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1376,7 +1376,7 @@ part of another hypothesis.") (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)") ) -(defun coq-detect-hyps-positions (buf) +(defun coq-detect-hyps-positions (buf &optional limit) "Detect all hypothesis displayed in buffer BUF and returns positions. 5 positions are created for each hyp: (begcross beghypname endhypname beg end)." @@ -1384,7 +1384,8 @@ endhypname beg end)." (save-excursion (goto-char (point-min)) (let ((res '())) - (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) + (goto-char (point-min)) + (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp limit t) (let* ((str (match-string 2)) (beghypname (match-beginning 2)) (beg (match-end 0)) @@ -1405,6 +1406,14 @@ endhypname beg end)." res)))) res)))) +;; Don't look at the conclusion of the goal +(defun coq-detect-hyps-positions-in-goals () + (with-current-buffer proof-goals-buffer + (goto-char (point-min)) + (coq-detect-hyps-positions + proof-goals-buffer + (if (search-forward-regexp "==========" nil t) (point) nil)))) + ;; We define a slightly different set of keywords for response buffer. diff --git a/coq/coq.el b/coq/coq.el index 55435aba..7f1dd378 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1500,12 +1500,12 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") res)) -(defun coq-detect-hyps (buf) +(defun coq-detect-hyps-in-goals () "Detect all hypothesis displayed in buffer BUF and returns a list overlays. Three overlays are created for each hyp: (hypov hypnameov hypcrossov), respectively for the whole hyp, only its name and the overlay for fold/unfold cross. " - (coq-build-hyps-overlays (coq-detect-hyps-positions buf) buf)) + (coq-build-hyps-overlays (coq-detect-hyps-positions-in-goals) proof-goals-buffer)) (defun coq-find-hyp-overlay (h) (cadr (assoc h coq-hyps-positions))) @@ -3048,7 +3048,7 @@ number of hypothesis displayed, without hiding the goal" (with-selected-window goal-win ;; find snd goal or buffer end, if not found this goes to the ;; end of buffer - (search-forward-regexp "subgoal 2\\|\\'") + (search-forward-regexp "subgoal 2\\|\\*\\*\\* Unfocused goals:\\|\\'") (beginning-of-line) ;; find something backward else than a space: bottom of concl (ignore-errors (search-backward-regexp "\\S-")) @@ -3107,7 +3107,7 @@ number of hypothesis displayed, without hiding the goal" (add-hook 'proof-shell-handle-delayed-output-hook (lambda () - (setq coq-hyps-positions (coq-detect-hyps proof-goals-buffer)) + (setq coq-hyps-positions (coq-detect-hyps-in-goals)) (coq-highlight-selected-hyps) (coq-fold-hyps) )) -- cgit v1.2.3