From 3c59de8fb17914708465ad4728d337c563e4e34f Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 1 Jun 2018 23:23:49 +0200 Subject: Click hypothesis to (un)hide them. --- CHANGES | 42 +++++++-- coq/coq-syntax.el | 15 ++- coq/coq.el | 266 ++++++++++++++++++++++++++++++++++++++++++------------ 3 files changed, 250 insertions(+), 73 deletions(-) diff --git a/CHANGES b/CHANGES index dad29f1b..13c51c10 100644 --- a/CHANGES +++ b/CHANGES @@ -60,21 +60,43 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac The set of tokens can be seen in variable smie-grammar. -*** Highlighting and hiding of hypothesis +*** Highlighting of hypothesis - A new mechanism to hide or highlight hypothesis (even if the goal - changes) in the goals buffer. This is meant to deal with large goals. + 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). - M-x coq-toggle-hide-hyp - M-x coq-toggle-hide-hyp-at-point + M-x coq-toggle-hide-hyp + M-x coq-toggle-hide-hyp-at-point (toggles hiding hyp at point) + M-x coq-unhide-hyps (unhides everything) - M-x coq-unhighlight-selected-hyps +**** 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. + + To disable this, do: + + (setq coq-highlight-hyps-cited-in-response nil) + +*** Hiding (folding) hypothesis + + 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. + + 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: - M-x coq-toggle-highlight-hyp - M-x coq-toggle-highlight-hyp-at-point + (setq coq-hypname-visible-hovering nil) - Hypothesis cited in the response buffer after a "About" command - (C-c C-a C-a) will be highlighted. + You will still be able to click them. **** Hypothesis cited in the response buffer. diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 61bb9751..a137115d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1358,7 +1358,7 @@ 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]\\|,$\\)\\)" + "\\(^\\|^ \\|^ \\|[^^ ] ? \\)\\(?:\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\) *\\(?::=?[ \n]\\|,$\\)\\)" "regexp matching hypothesis names in goal or response buffer") (defvar coq-hyp-name-or-goalsep-in-goal-or-response-regexp @@ -1366,6 +1366,9 @@ It is used: ) (defun coq-detect-hyps (buf) + "Detect all hypothesis displayed in buffer BUF and returns a list of descriptors. +Descriptors are of the form (hypname start end endofhypname) +where end is the end of the hypothesis type." (with-current-buffer buf (save-excursion (goto-char (point-min)) @@ -1373,12 +1376,18 @@ It is used: (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) (let* ((str (match-string 2)) (beg (match-beginning 2)) + (endhypname (match-end 2)) (splitstr (split-string str ",\\|,$\\|:" t "\\s-")) (end (save-excursion (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t) (match-beginning 0)))) - (mapcar - (lambda (s) (setq res (cons (cons (substring-no-properties s) (cons beg (cons end nil))) res))) + (mapc + (lambda (s) + (setq res + (cons + (cons (substring-no-properties s) + (cons beg (cons end (cons endhypname nil)))) + res))) splitstr))) ;; TODO: register thje last hyp. res)))) diff --git a/coq/coq.el b/coq/coq.el index 52782fa9..e4a289c1 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -53,7 +53,6 @@ (require 'coq-seq-compile) ; sequential compilation of Requires (require 'coq-par-compile) ; parallel compilation of Requires - ;; for compilation in Emacs < 23.3 (NB: declare function only works at top level) (declare-function smie-bnf->prec2 "smie") (declare-function smie-rule-parent-p "smie") @@ -1056,19 +1055,6 @@ This is specific to `coq-mode'." (interactive) (coq-ask-do "SearchRewrite" "SearchRewrite" nil)) -;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old. -(defun coq-SearchAbout () - (interactive) - (coq-ask-do - ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns: - ;; "_ind" "_rec" "R_" "_equation" - "SearchAbout (ex: \"eq_\" eq -bool)" - "SearchAbout" - nil nil t) - ; uncomment to highlight hyps cites in "About"'s result. - (coq-highlight-hyps-cited-in-response) - (message "M-x coq-unhighlight-selected-hyps to remove highlighting, [Coq/Settings/Search Blacklist] to change blacklisting.") - ) @@ -1376,28 +1362,48 @@ goal is redisplayed." (rd (read-number (format "Width (%S): " deflt) deflt))) (coq-adapt-printing-width t rd))) -;;;;;;;;;;;;;; Highlighting hypothesis ;;;;;;;; -(defvar coq-hyps-positions nil) -(defvar coq-highlighted-hyps nil) +;;;;; utils fo overlays +(defun coq-overlays-at (pt prop) + (let ((overlays (overlays-at pt)) + found) + (while overlays + (let ((overlay (car overlays))) + (if (overlay-get overlay prop) + (setq found (cons overlay found)))) + (setq overlays (cdr overlays))) + found)) + +;;;;;;;;;; Hypothesis tracking ;;;;;;;;;; +;;; Facilities to build overlays for hyp names and hyp+type. +;;; These are built on-demand: +;; - hyp names overlays are always (proof-shell-handle-delayed-output-hook) +;; - hyp+type overlays are built when hiding a hypothesis, then it is not +;; destroyed until the goals buffer is changed + +(defvar coq-hyps-positions nil + "The list of positions of hypothesis in the goals buffer. +Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") (defun coq-find-hyp-overlay (h) + "Finds the hyp+type overlay for hyp H, or nil." (let* ((hyp-pos (assoc h coq-hyps-positions)) (hyp-beg (cadr hyp-pos)) (hyp-end (caddr hyp-pos)) (hyp-overlay-already (and hyp-beg (car (with-current-buffer proof-goals-buffer - (overlays-at hyp-beg 'hyp)))))) + (coq-overlays-at hyp-beg 'hyp)))))) hyp-overlay-already)) (defun coq-find-or-create-hyp-overlay (h) + "Finds the hyp+type overlay for hyp H, or create one." (let* ((hyp-pos (assoc h coq-hyps-positions)) (hyp-beg (cadr hyp-pos)) (hyp-end (caddr hyp-pos)) (hyp-overlay-already (and hyp-beg (car (with-current-buffer proof-goals-buffer - (overlays-at hyp-beg 'hyp))))) + (coq-overlays-at hyp-beg 'hyp))))) (hyp-overlay (and hyp-beg hyp-end (or hyp-overlay-already (make-overlay hyp-beg hyp-end proof-goals-buffer))))) @@ -1405,53 +1411,115 @@ goal is redisplayed." (and hyp-overlay (overlay-put hyp-overlay 'hyp t)) hyp-overlay)) +(defun coq-find-hypname-overlay (h) + "Finds the hyp name overlay for hyp H." + (let* ((hyp-pos (assoc h coq-hyps-positions)) + (hyp-beg (cadr hyp-pos)) + (hyp-end (cadddr hyp-pos)) + (hyp-overlay-already + (and hyp-beg + (car (with-current-buffer proof-goals-buffer + (coq-overlays-at hyp-beg 'hypname)))))) + hyp-overlay-already)) + +(defun coq-find-or-create-hypname-overlay (h) + "Finds the hyp name overlay for hyp H, or create one." + (let* ((hyp-pos (assoc h coq-hyps-positions)) + (hyp-beg (cadr hyp-pos)) + (hyp-end (cadddr hyp-pos)) + (hyp-overlay-already + (and hyp-beg + (car (with-current-buffer proof-goals-buffer + (coq-overlays-at hyp-beg 'hypname))))) + (hyp-overlay (and hyp-beg hyp-end + (or hyp-overlay-already + (make-overlay hyp-beg hyp-end proof-goals-buffer))))) + ;; if it was just created + (and hyp-overlay (overlay-put hyp-overlay 'hypname t)) + hyp-overlay)) + + +;;;;;;;;;;;;;; Highlighting hypothesis ;;;;;;;; +;; Feature: highlighting of hyptohesis that remains when the cript is played +;; (and goals buffer is updated). + +;; On by default. This only works with the SearchAbout function for now. +(defvar coq-highlight-hyps-cited-in-response t + "If non-nil, try to highlight in goals buffers cited hyps response.") + +;; We maintain a list of hypothesis names that must be highlighted at each +;; regeneration of goals buffer. +(defvar coq-highlighted-hyps nil + "List of hypothesis names that must be highlighted. +These are rehighlighted at each regeneration of goals buffer +using a hook in `proof-shell-handle-delayed-output-hook'.") + (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 +buffer is updated." (let ((hyp-overlay (coq-find-or-create-hyp-overlay h))) (when hyp-overlay (overlay-put hyp-overlay 'face '(:background "lavender")) (overlay-put hyp-overlay 'invisible nil)))) (defun coq-unhighlight-hyp-aux (h) + "Auxiliary function, use `coq-unhighlight-hyp' for sticky highlighting. +Unless you want the highlighting to disappear after the goals +buffer is updated." (let* ((hyp-overlay-already (coq-find-hyp-overlay h))) (when hyp-overlay-already (overlay-put hyp-overlay-already 'face '(:background "unspecified-bg"))))) (defun coq-highlight-hyp (h) + "Highlight hypothesis named H (sticky). +use `coq-unhighlight-hyp' to unhilight." (unless (member h coq-highlighted-hyps) (setq coq-highlighted-hyps (cons h coq-highlighted-hyps))) (coq-highlight-hyp-aux h)) -(defun coq-highlight-hyps (lh) - (mapcar 'coq-highlight-hyp lh)) - -(defun coq-highlight-selected-hyps () - (interactive) - (coq-highlight-hyps coq-highlighted-hyps)) - (defun coq-unhighlight-hyp (h) + "Unhighlight hypothesis named H." (when (member h coq-highlighted-hyps) (setq coq-highlighted-hyps (delete h coq-highlighted-hyps)) (coq-unhighlight-hyp-aux h))) +(defun coq-highlight-hyps (lh) + (mapc 'coq-highlight-hyp lh)) + (defun coq-unhighlight-hyps (lh) - (mapcar 'coq-unhighlight-hyp-aux lh)) + (mapc 'coq-unhighlight-hyp-aux lh)) + +(defun coq-highlight-selected-hyps () + "Highlight all hyps stored in `coq-highlighted-hyps'. +This used in hook to rehilight hypothesis after goals buffer is +updated." + (interactive) + (coq-highlight-hyps coq-highlighted-hyps)) (defun coq-unhighlight-selected-hyps () + "Unhighlight all hyps stored in `coq-highlighted-hyps'. +This used before updating `coq-highlighted-hyps' with a new set +of hypothesis to highlight." (interactive) (coq-unhighlight-hyps coq-highlighted-hyps) (setq coq-highlighted-hyps nil)) (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))) (remove-if-not (lambda (e) - (seq-find + (cl-some;seq-find (lambda (f) (string-equal (car e) (car f))) hyps-cited)) coq-hyps-positions))) (defun coq-highlight-hyps-cited-in-response () + "Highlight hypothesis cited in response buffer. +Highlight always takes place in goals buffer." (let ((inters (coq-get-hyps-cited-in-response))) (coq-unhighlight-selected-hyps) (setq coq-highlighted-hyps (mapcar 'car inters)) @@ -1465,50 +1533,105 @@ See `coq-highlight-hyp'." (coq-unhighlight-hyp h) (coq-highlight-hyp h))) -(defun coq-toggle-highlight-hyp-at-point () +(defun coq-highlight () "Toggle the hiding status of hypothesis H whose name is at point. See `coq-hide-hyp'." (interactive) (coq-toggle-highlight-hyp (substring-no-properties (coq-id-or-notation-at-point)))) -;;;;;;;;;;;;;;;;;; - -(defvar coq-highlight-id-last-regexp nil) - -(defun coq-highlight-id-in-goals (re) - (with-current-buffer proof-goals-buffer - (highlight-regexp re 'lazy-highlight))) - -(defun coq-highlight-hyp-in-goals (re) - (with-current-buffer proof-goals-buffer - (highlight-regexp (concat " [^[:blank:]].+" re ".+\n [^[:blank:]]") 'lazy-highlight))) - -(defun coq-unhighlight-id-in-goals (re) - (with-current-buffer proof-goals-buffer - (unhighlight-regexp re))) - -(defun coq-highlight-id-at-pt-in-goals () +;;;;;;;;;;; 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.") + +(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 +using a hook in `proof-shell-handle-delayed-output-hook'.") + +(defun coq-toggle-hide-hyp-at (pt) + "Toggle hiding the hypothesis at point." (interactive) - (let* ((id (coq-id-or-notation-at-point)) - (re (regexp-quote (or id "")))) - (when coq-highlight-id-last-regexp - (coq-unhighlight-id-in-goals coq-highlight-id-last-regexp)) - (coq-highlight-id-in-goals re) - (setq coq-highlight-id-last-regexp re))) + (let ((hypname + (or + (overlay-get (car (coq-overlays-at pt 'is-hyp-name)) 'hyp-name) + (overlay-get (car (coq-overlays-at pt 'hyp)) 'hyp-name)))) + (if (member hypname coq-hidden-hyps) + (coq-unhide-hyp hypname) + (coq-hide-hyp hypname)))) +(defun coq-toggle-hide-hyp-at-point () + (coq-toggle-hide-hyp-at (point))) -;;;; Hiding variables -(defvar coq-hidden-hyps nil) +(defun coq-toggle-hide-hyp-at-mouse (event) + "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. +(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)) + +(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)) + (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 'hyp-name h) + (overlay-put hyp-overlay 'keymap coq-hidden-hyp-map))) + +(defun coq-configure-hyp-overlay-visible (hyp-overlay h) + (when hyp-overlay + (overlay-put hyp-overlay 'display nil) + (overlay-put hyp-overlay 'evaporate t) + (overlay-put hyp-overlay 'mouse-face nil) + (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 +Displays \".......\" instead. This function relies on variable coq-hyps-positions. The hiding is cancelled as soon as the goals buffer is changed, consider using `coq-hide-hyp' if you want the hiding to be maintain when scripting/undoing." (let ((hyp-overlay (coq-find-or-create-hyp-overlay h))) - (when hyp-overlay (overlay-put hyp-overlay 'display (concat h ": ......."))))) + (when hyp-overlay (coq-configure-hyp-overlay-hidden hyp-overlay h)))) (defun coq-hide-hyp (h) "Hide hypothesis H's type from the context durably. @@ -1527,7 +1650,7 @@ scripting/undoing." "Unhide hypothesis H temporarily. See `coq-hide-hyp-aux'." (let ((hyp-overlay (coq-find-or-create-hyp-overlay h))) - (when hyp-overlay (overlay-put hyp-overlay 'display nil)))) + (coq-configure-hyp-overlay-visible hyp-overlay h))) (defun coq-unhide-hyp (h) "Unhide hypothesis H durably. @@ -1540,12 +1663,12 @@ See `coq-hide-hyp'." (defun coq-unhide-hyp-list (lh) "Hide the type of hypothesis in LH temporarily. See `coq-unhide-hyp-aux'." - (mapcar 'coq-unhide-hyp-aux lh)) + (mapc 'coq-unhide-hyp-aux lh)) (defun coq-hide-hyp-list (lh) "Hide the type of hypothesis in LH temporarily. See `coq-hide-hyp-aux'." - (mapcar 'coq-hide-hyp-aux lh)) + (mapc 'coq-hide-hyp-aux lh)) (defun coq-hide-hyps () "Hide the type of hypothesis in LH durably. @@ -1561,8 +1684,15 @@ See `coq-unhide-hyp'." (coq-unhide-hyp-list coq-hidden-hyps) (setq coq-hidden-hyps nil)) +(defun coq-init-hypname-overlays (lh) + "(re)generate the overlays on hyps names. +These overlays are used to allow hiding hypothesis by clicking on +its name (button 3 should be the default). This is called by a +hook in `proof-shell-handle-delayed-output-hook'." + (mapc 'coq-init-hypname-overlay (mapcar 'car lh))) + (defun coq-toggle-hide-hyp (h) - "Toggle the hiding status of hypothesis H. + "Toggle the hiding status of hypothesis H (asked interactively). See `coq-hide-hyp'." (interactive "sHypothesis to hide: ") (if (member h coq-hidden-hyps) @@ -2591,6 +2721,21 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (proof-shell-invisible-command q)))) +;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old. +(defun coq-SearchAbout () + (interactive) + (coq-ask-do + ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns: + ;; "_ind" "_rec" "R_" "_equation" + "SearchAbout (ex: \"eq_\" eq -bool)" + "SearchAbout" + nil nil t) + (when coq-highlight-hyps-cited-in-response + (coq-highlight-hyps-cited-in-response) + (message "M-x coq-unhighlight-selected-hyps to remove highlighting, [Coq/Settings/Search Blacklist] to change blacklisting.")) + (unless coq-highlight-hyps-cited-in-response + (message "[Coq/Settings/Search Blacklist] to change blacklisting."))) + ;; Insertion commands (define-key coq-keymap [(control ?i)] 'coq-insert-intros) (define-key coq-keymap [(control ?m)] 'coq-insert-match) @@ -2882,6 +3027,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)) + (coq-init-hypname-overlays coq-hyps-positions) (coq-highlight-selected-hyps) (coq-hide-hyps))) -- cgit v1.2.3