From e1af53a09165d2e3e16b977fe73741d20a708a29 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Mon, 11 Jun 2018 12:03:37 +0200
Subject: key maps + small glitch hyp highlight/folding code.

---
 CHANGES    | 10 ++++++----
 coq/coq.el | 29 ++++++++++++++++++++++++++---
 2 files changed, 32 insertions(+), 7 deletions(-)

diff --git a/CHANGES b/CHANGES
index beb70480..e7343e08 100644
--- a/CHANGES
+++ b/CHANGES
@@ -60,7 +60,7 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     
     The set of tokens can be seen in variable smie-grammar.
 
-*** Clickable Hypothesis in goals buffer
+*** Clickable Hypothesis in goals buffer to copy/paste hyp names
 
     Clicking on a hyp name in goals buffer with button 2 copies its
     name at current point position (which should be in the scripting
@@ -70,15 +70,17 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
 
    A cross "-" is displayed to the left of each hypothesis of the
    goals buffer. Clicking ont it (button 1) hides/unhides the
-   hypothesis. You can also hit "f" while ont he hypothesis.
+   hypothesis. You can also hit "f" while ont he hypothesis. "F"
+   unfolds all hypothesis.
    
    Hide/ unhide status remains when goal changes.
 
 
 *** Highlighting of hypothesis
 
-    You can highlight hypothesis on a per name fashion. Hit "h" while
-    on the hypothesis.
+    You can highlight hypothesis in goals buffer on a per name
+    fashion. Hit "h" while on the hypothesis. "H" removes all
+    highlighting in the buffer.
 
     Highlighting status remains when goal changes.
 
diff --git a/coq/coq.el b/coq/coq.el
index ac2c59f2..bf34f6aa 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1471,10 +1471,30 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
 (defun coq-build-hyps-overlays (hyp-positions buf)
   (let ((res))
     (mapc (lambda (x) (let ((lassoc (coq-build-hyp-overlay x buf)))
-                      (setq res (append lassoc res))))
+                        (setq res (append lassoc res))))
           hyp-positions)
     res))
 
+; builds the list of names from one hyp position (which may contained several
+; hyp names)
+(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)
+    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 (buf)
   "Detect all hypothesis displayed in buffer BUF and returns a list overlays.
 Three overlays are created for each hyp: (hypov hypnameov hypcrossov), respectively
@@ -1517,6 +1537,7 @@ using a hook in `proof-shell-handle-delayed-output-hook'.")
 
 (when coq-hypname-map 
   (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse)
+  (define-key coq-hypcross-map [return] 'coq-toggle-fold-hyp-at-point)
   (define-key coq-hypcross-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse))
 
 (defun coq-highlight-hyp-aux (h)
@@ -1573,12 +1594,13 @@ of hypothesis to highlight."
 (defun coq-get-hyps-cited-in-response ()
   "Returns locations of hyps in goals buffer that are cited in response buffer.
 See `coq-highlight-hyps-cited-in-response' and `SearchAbout'."
-  (let ((hyps-cited (coq-detect-hyps proof-response-buffer)))
+  (let* ((hyps-cited-pos (coq-detect-hyps-positions proof-response-buffer))
+         (hyps-cited (coq-build-hyps-names hyps-cited-pos)))
     (remove-if-not
      (lambda (e)
        (cl-some;seq-find
         (lambda (f)
-          (string-equal (car e) (car f)))
+          (string-equal (car e) f))
         hyps-cited))
      coq-hyps-positions)))
 
@@ -2841,6 +2863,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?n)] 'coq-LocateNotation)
 ;; specific to goals buffer: (un)foldinng and (un)highlighting shortcuts
 (define-key coq-goals-mode-map [?f] 'coq-toggle-fold-hyp-at-point)
+(define-key coq-goals-mode-map [?F] 'coq-unfold-hyps)
 (define-key coq-goals-mode-map [?h] 'coq-toggle-highlight-hyp-at-point)
 (define-key coq-goals-mode-map [?H] 'coq-unhighlight-selected-hyps)
 
-- 
cgit v1.2.3