Shorter CHANGES + smal fixes in hide/highlight hyps code.

3 files changed, 93 insertions, 69 deletions

diff --git a/CHANGES b/CHANGES
index 13c51c10..7943ca50 100644
--- a/CHANGES
+++ b/CHANGES
@@ -60,45 +60,45 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     
     The set of tokens can be seen in variable smie-grammar.
 
-*** Highlighting of hypothesis
+*** Clickable Hypothesis in goals buffer
+
+    button 3 on a hyp name hides/unhides it (fold/unfold). 
+    button 2 on a hyp name copies its name at current cursor position.
 
-    This is meant to deal with large goals. Highlighting is done on a
-    per hyp name fashion. Once a hypothesis is tagged as highlighted
-    it remains highlighted until you unihghlight it or another set of
-    hyps is highlighted (see below). 
+    hide/unhide status remains when goal changes.
 
-    M-x coq-toggle-hide-hyp 
+    You can define keyboard shortcuts for these:
+
+    M-x coq-toggle-hide-hyp (asks for a hyp name)
     M-x coq-toggle-hide-hyp-at-point (toggles hiding hyp at point)
     M-x coq-unhide-hyps (unhides everything)
 
-**** Automtic highlighting with (search)About.
-    Hypothesis cited in the response buffer after (C-c C-a C-a) (M-x
-    coq-SearchAbout) will be highlighted automatically. Any other
-    hypothesis highlighted is unhighlighted.
+    By default hypothesis names are highlighted when hovered with the
+    mouse, and a small help also pops up. you can disable it with on
+    of these:
     
-    To disable this, do:
+     (setq coq-hypname-visible-hovering 'only-help) 
+     (setq coq-hypname-visible-hovering 'only-highlight) 
+     (setq coq-hypname-visible-hovering nil) ;; nothing
+     (setq coq-hypname-visible-hovering t) ;; both, default
 
-    (setq coq-highlight-hyps-cited-in-response nil)
+*** Highlighting of hypothesis
 
-*** Hiding (folding) hypothesis
+    you can highlight hypothesis on a per name fashion. 
 
-    This is meant to deal with large goals. Hiding is done on a per
-    hyp name fashion. Once a hypothesis is tagged as hidden it remains
-    hidden until you.
+    Highlighting status remains when goal changes.
 
+    M-x coq-highlight (toggles highlighting on hyp at point)
     M-x coq-unhighlight-selected-hyps (removes all highlightings)
-    M-x coq-highlight (toggles highlighting onhyp at point)
 
-**** Click on a hyp to hide/unhide it
-    Hyptohesis names are now clickable (button 3) to be (un)hidden.
-    If you don't like the highlighting of hyp names when hovering it,
-    you can use:
-
-    (setq coq-hypname-visible-hovering nil)
-
-    You will still be able to click them.
+**** Automtic highlighting with (search)About.
+    Hypothesis cited in the response buffer after C-c C-a C-a (i.e.
+    M-x coq-SearchAbout) will be highlighted automatically. Any other
+    hypothesis highlighted is unhighlighted.
+    
+    To disable this, do:
 
-**** Hypothesis cited in the response buffer.
+    (setq coq-highlight-hyps-cited-in-response nil)
 
 *** bug fixes
     - avoid leaving partial files behind when compilation fails
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a137115d..c24b63f9 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1358,11 +1358,15 @@ It is used:
 ;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5)
 ;; "^    " is for goals in debug mode.
 (defvar coq-hyp-name-in-goal-or-response-regexp
-    "\\(^\\|^  \\|^    \\|[^^ ] ?  \\)\\(?:\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\) *\\(?::=?[ \n]\\|,$\\)\\)"
-  "regexp matching hypothesis names in goal or response buffer")
+    "\\(?:\\(?1:\n\\)\\|\\(?1:\n  \\)\\|\\(?1:\n    \\)\\|\\(?:[^ ]\\)\\(?1:   \\)\\)\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\) *\\(?::=?[ \n]\\|,$\\)"
+  "regexp matching hypothesis names in goal or response buffer.
+Subexpr 2 contains the real name of the function.
+Subexpr 1 contains the prefix context (spaces mainly) that is not
+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 "\\|\n\\s-+========")
+  (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:\n\\s-+========\\)")
   )
 
 (defun coq-detect-hyps (buf)
@@ -1378,9 +1382,9 @@ where end is the end of the hypothesis type."
                  (beg (match-beginning 2))
                  (endhypname (match-end 2))
                  (splitstr (split-string str ",\\|,$\\|:" t "\\s-"))
-                 (end (save-excursion
+                 (end (save-excursion ; looking for next hyp and return its leftest part
                         (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t)
-                        (match-beginning 0))))
+                        (match-beginning 1))))
             (mapc
              (lambda (s)
                (setq res
@@ -1389,7 +1393,6 @@ where end is the end of the hypothesis type."
                             (cons beg (cons end (cons endhypname nil))))
                       res)))
              splitstr)))
-        ;; TODO: register thje last hyp.
         res))))
 
 ;; We define a slightly different set of keywords for response buffer.
diff --git a/coq/coq.el b/coq/coq.el
index e4a289c1..f072a716 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1447,6 +1447,15 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
 (defvar coq-highlight-hyps-cited-in-response t
   "If non-nil, try to highlight in goals buffers cited hyps response.")
 
+(defvar coq-hypname-visible-hovering t
+  "Whether hyp name overlays should be visible, and a help popup.
+In goals buffer, each hypothesis name has a clickable overlay.
+Making it highlited when hovering with mouse is nice to advertise
+the feature, but some people are allergic to this kind of
+distracting flickering. Possible values are: 'only-help,
+'only-highlight, nil, or t. Default is t, which means have both
+highlight and help echo.")
+
 ;; We maintain a list of hypothesis names that must be highlighted at each
 ;; regeneration of goals buffer.
 (defvar coq-highlighted-hyps nil
@@ -1454,6 +1463,12 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
 These are rehighlighted at each regeneration of goals buffer
 using a hook in `proof-shell-handle-delayed-output-hook'.")
 
+(defvar coq-hypname-map (make-sparse-keymap) "Keymap for visible hypothesis")
+;; Ddefault binding: clicking on the name of an hyp hides it.
+(when coq-hypname-map 
+  (define-key coq-hypname-map [(mouse-3)] 'coq-toggle-hide-hyp-at-mouse)
+  (define-key coq-hypname-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse))
+
 (defun coq-highlight-hyp-aux (h)
   "Auxiliary function, use `coq-highlight-hyp' for sticky highlighting.
 Unless you want the highlighting to disappear after the goals
@@ -1540,14 +1555,37 @@ See  `coq-hide-hyp'."
   (coq-toggle-highlight-hyp
    (substring-no-properties (coq-id-or-notation-at-point))))
 
-;;;;;;;;;;; Hiding Hypothesis  ;;;;;;;;;;;
-(defvar coq-hypname-visible-hovering t
-  "Whether hyp name overlays should be visible.
-In goals buffer, each hypothesis name has an clickable overlay.
-Making it highlited when thover the mouse on them is nice to
-advertise the feature, but some people are allergic to this kind
-of distracting flickering.")
 
+(defun coq-configure-hypname-overlay (hyp-overlay h)
+  (when hyp-overlay
+    (overlay-put hyp-overlay 'evaporate t)
+    (overlay-put hyp-overlay 'is-hyp-name t)
+    (overlay-put hyp-overlay 'hyp-name h)
+    ;; only for non allergic
+    (cond 
+     ((eq coq-hypname-visible-hovering 'only-help)
+      (overlay-put hyp-overlay 'help-echo "mouse-3: unhide; mouse-2 copy name"))
+     ((eq coq-hypname-visible-hovering 'only-highlight)
+      (overlay-put hyp-overlay 'mouse-face 'proof-command-mouse-highlight-face))
+     ((eq coq-hypname-visible-hovering t)
+      (overlay-put hyp-overlay 'mouse-face 'proof-command-mouse-highlight-face)
+      (overlay-put hyp-overlay 'help-echo "mouse-3: unhide; mouse-2 copy name")))
+    (overlay-put hyp-overlay 'keymap coq-hypname-map))
+  hyp-overlay)
+
+(defun coq-init-hypname-overlay (h)
+  (coq-configure-hypname-overlay (coq-find-or-create-hypname-overlay h) h))
+
+(defun coq-insert-at-point-hyp-at-mouse (event)
+  (interactive "e")
+  (let ((hyp-name (save-excursion
+                    (with-current-buffer proof-goals-buffer
+                      (save-excursion
+                        (overlay-get (car (overlays-at (posn-point (event-start event))))
+                                     'hyp-name))))))
+    (insert hyp-name)))
+
+;;;;;;;;;;; Hiding Hypothesis  ;;;;;;;;;;;
 (defvar coq-hidden-hyps nil
   "List of hypothesis that should be hidden in goals buffer.
 These are re-hidden at each regeneration of goals buffer
@@ -1571,33 +1609,31 @@ using a hook in `proof-shell-handle-delayed-output-hook'.")
   "Toggle hiding the hypothesis at mouse click.
 Used on hyptohesis overlays in goals buffer mainly."
   (interactive "e")
-  (message "pos: %s" (posn-point (event-start event)))
   (save-excursion
     (with-current-buffer proof-goals-buffer
       (save-excursion (coq-toggle-hide-hyp-at (posn-point (event-start event)))))))
 
 (defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden hypothesis")
-(defvar coq-hypname-map (make-sparse-keymap) "Keymap for visible hypothesis")
 
-;; Ddefault binding: clicking on a hidden hyp with button 3 unhides it.
+;; Ddefault binding: clicking on a hidden hyp with button 3 unhides it, with
+;; button 2 it copies hyp name at current point.
 (when coq-hidden-hyp-map 
-  (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-hide-hyp-at-mouse))
-
-;; Ddefault binding: clicking on the name of an hyp hides it.
-(when coq-hypname-map 
-  (define-key coq-hypname-map [(mouse-3)] 'coq-toggle-hide-hyp-at-mouse))
-
-(defun coq-build-hidden-hyp-string (h)
-  (propertize (concat h ": .......") 'keymap coq-hidden-hyp-map))
+  (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-hide-hyp-at-mouse)
+  (define-key coq-hidden-hyp-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse))
 
 (defun coq-configure-hyp-overlay-hidden (hyp-overlay h)
   (when hyp-overlay
-    (overlay-put
-     hyp-overlay 'display 
-     (propertize (concat h ": .......") 'keymap coq-hidden-hyp-map))
+    (let ((prefx (save-excursion
+                   (with-current-buffer proof-goals-buffer
+                     (goto-char (overlay-start hyp-overlay))
+                     (search-forward-regexp ":")
+                     (if (looking-at "=") (concat h " := .......") (concat h " : ........"))))))
+      (overlay-put
+       hyp-overlay 'display 
+       (propertize prefx 'keymap coq-hidden-hyp-map)))
     (overlay-put hyp-overlay 'evaporate t)
     (overlay-put hyp-overlay 'mouse-face 'proof-command-mouse-highlight-face)
-    (overlay-put hyp-overlay 'help-echo "mouse-3: unhide")
+    (overlay-put hyp-overlay 'help-echo "mouse-3: unhide; mouse-2 copy name")
     (overlay-put hyp-overlay 'hyp-name h)
     (overlay-put hyp-overlay 'keymap coq-hidden-hyp-map)))
 
@@ -1609,21 +1645,6 @@ Used on hyptohesis overlays in goals buffer mainly."
     (overlay-put hyp-overlay 'help-echo nil)
     (overlay-put hyp-overlay 'keymap nil)))
 
-(defun coq-configure-hypname-overlay (hyp-overlay h)
-  (when hyp-overlay
-    (overlay-put hyp-overlay 'evaporate t)
-    (overlay-put hyp-overlay 'is-hyp-name t)
-    (overlay-put hyp-overlay 'hyp-name h)
-    ;; only for non allergic
-    (when coq-hypname-visible-hovering
-      (overlay-put hyp-overlay 'mouse-face 'proof-command-mouse-highlight-face)
-      (overlay-put hyp-overlay 'help-echo "mouse-3: hide"))
-    (overlay-put hyp-overlay 'keymap coq-hypname-map))
-  hyp-overlay)
-
-(defun coq-init-hypname-overlay (h)
-  (coq-configure-hypname-overlay (coq-find-or-create-hypname-overlay h) h))
-
 (defun coq-hide-hyp-aux (h)
   "Hide hypothesis H's type from the context temporarily.
 Displays \".......\" instead. This function relies on variable