Fix multiple hyp overlays.

queries would trigger re-generarion of overlays. Now overlays are
generated if there are no overlays already.

2 files changed, 17 insertions, 8 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5b12bd8e..d6850a0a 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1373,8 +1373,14 @@ part of another hypothesis.")
 
 ; Matches the end of the last hyp, before the ======... separator.
 (defvar coq-hyp-name-or-goalsep-in-goal-or-response-regexp
-  (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)")
-  )
+  (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)"))
+
+(defun coq-find-first-hyp ()
+  (with-current-buffer proof-goals-buffer
+    (save-excursion
+      (goto-char (point-min))
+      (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t)
+      (match-beginning 2))))
 
 (defun coq-detect-hyps-positions (buf &optional limit)
   "Detect all hypothesis displayed in buffer BUF and returns positions.
diff --git a/coq/coq.el b/coq/coq.el
index 7f1dd378..1a9feb2d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1485,27 +1485,30 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
 (defun coq-build-hyp-name (hyp-positions)
   (let* ((names (car hyp-positions))
          res)
-    (message "names = %S" names)
-    (mapc (lambda (s) (setq res (cons (substring-no-properties s) res))) names)
-    (message "res = %S" res)
+   (mapc (lambda (s) (setq res (cons (substring-no-properties s) res))) names)
     res))
 
 ;; Build the list of hyps names
 (defun coq-build-hyps-names (hyp-positions)
   (let ((res))
     (mapc (lambda (x) (let ((lassoc (coq-build-hyp-name x)))
-                        (message "lassoc = %S" lassoc)
                         (setq res (append lassoc res))))
           hyp-positions)
     res))
 
 
 (defun coq-detect-hyps-in-goals ()
-  "Detect all hypothesis displayed in buffer BUF and returns a list overlays.
+  "Detect all hypothesis displayed in goals buffer and create 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.
+Returnns the list of mappings hypname -> overlays.
 "
-  (coq-build-hyps-overlays (coq-detect-hyps-positions-in-goals) proof-goals-buffer))
+  (let*
+      ((fsthyp-pos (coq-find-first-hyp))
+       (fsthyp-ov (when fsthyp-pos (with-current-buffer proof-goals-buffer
+                                     (overlays-at fsthyp-pos)))))
+    (if fsthyp-ov coq-hyps-positions ;overlays are already there
+      (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)))