Fix the fix #355.

The fix was bad: no ore hyps were foldable/highlightable.

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)
             ))