From c4b49a4a3e7b5206f1f29495fd96980aad73e5b9 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 8 Jun 2018 18:19:29 +0200 Subject: Changed the look of folding/unfolding hyps. --- CHANGES | 30 ++--- coq/coq-db.el | 22 +++ coq/coq-syntax.el | 36 ++--- coq/coq.el | 392 ++++++++++++++++++++++++++++++------------------------ 4 files changed, 268 insertions(+), 212 deletions(-) diff --git a/CHANGES b/CHANGES index 7943ca50..beb70480 100644 --- a/CHANGES +++ b/CHANGES @@ -62,34 +62,26 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac *** 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. + Clicking on a hyp name in goals buffer with button 2 copies its + name at current point position (which should be in the scripting + buffer). This eases the insertion of hypothesis names in scripts. - hide/unhide status remains when goal changes. +*** Folding/unfolding hypothesis - You can define keyboard shortcuts for these: + 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. + + Hide/ unhide status remains when goal changes. - 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) - - 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: - - (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 *** Highlighting of hypothesis - you can highlight hypothesis on a per name fashion. + You can highlight hypothesis on a per name fashion. Hit "h" while + on the hypothesis. 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) **** Automtic highlighting with (search)About. Hypothesis cited in the response buffer after C-c C-a C-a (i.e. diff --git a/coq/coq-db.el b/coq/coq-db.el index 28f2ff2b..dccdca52 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -330,6 +330,28 @@ See `coq-syntax-db' for DB structure." "Face used for `ltac:', `constr:', and `uconstr:' headers." :group 'proof-faces) +;; This messes columns, can't figure out why putting this face makes the overlay +;; larger than a character +;; (defface coq-button-face +;; '((t :inherit custom-button :background "dark gray")) +;; "" +;; :group 'proof-faces) + +;; (defface coq-button-face-pressed +;; '((t :inherit custom-button-pressed :background "light gray")) +;; "" +;; :group 'proof-faces) + +(defface coq-button-face + '((t . (:background "light gray"))) + "" + :group 'proof-faces) + +(defface coq-button-face-pressed + '((t . (:background "dark gray"))) + "" + :group 'proof-faces) + (defconst coq-solve-tactics-face 'coq-solve-tactics-face "Expression that evaluates to a face. Required so that 'coq-solve-tactics-face is a proper facename") diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5219afa7..4bc8d984 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1365,7 +1365,7 @@ It is used: ;; we used to have: "^ " for goals in debug mode but it does not seem ;; necessary anymore. (defvar coq-hyp-name-in-goal-or-response-regexp - "\\(?:\\(?1:^\\)\\|\\(?1:^ \\)\\|\\(?:[^ ]\\)\\(?1: \\)\\)\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\) *\\(?::=?[ \n]\\|,$\\)" + "\\(?:\\(?1:^\\)\\|\\(?1:^ \\)\\|\\(?:[^ ] \\)\\(?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 @@ -1373,35 +1373,39 @@ 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:\n\\s-+========\\)") + (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)") ) -(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." +(defun coq-detect-hyps-positions (buf) + "Detect all hypothesis displayed in buffer BUF and returns positions. +5 positions are created for each hyp: (begcross beghypname +endhypname beg end)." (with-current-buffer buf (save-excursion (goto-char (point-min)) (let ((res '())) (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) (let* ((str (match-string 2)) - (beg (match-beginning 2)) + (beghypname (match-beginning 2)) + (beg (match-end 0)) + (begcross (match-beginning 1)) (endhypname (match-end 2)) (splitstr (split-string str ",\\|,$\\|:" t "\\s-")) (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 1)))) - (mapc - (lambda (s) - (setq res - (cons - (cons (substring-no-properties s) - (cons beg (cons end (cons endhypname nil)))) - res))) - splitstr))) + (goto-char (match-beginning 1)) + ;; if previous is a newline, don't include it i the overklay + (when (looking-back "\\s-") (goto-char (- (point) 1))) + (point)))) + ; if several hyp names, we name the overlays with the first hyp name + (setq res + (cons + (cons (mapcar (lambda (s) (substring-no-properties s)) splitstr) + (list begcross beghypname endhypname beg end)) + res)))) res)))) + ;; We define a slightly different set of keywords for response buffer. (defvar coq-response-font-lock-keywords diff --git a/coq/coq.el b/coq/coq.el index f072a716..ac2c59f2 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1374,70 +1374,116 @@ goal is redisplayed." 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 +;;; Facilities to build overlays for hyp names and hyp+type + hypcross +;;; ((un)folding buttons). (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 - (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 - (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))))) - ;; if it was just created - (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)) +;; Hyps name are clickable and have a special keymap. +(defun coq-make-hypname-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hypname t) + (overlay-put ov 'hyp-name h) + (overlay-put ov 'keymap coq-hypname-map)) + ov)) + +;; Hyps types are clickable only when folded +(defun coq-make-hyp-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hyp t) + (overlay-put ov 'hyp-name h)) + ov)) + +(defun coq-hypcross-unfolded-string() + (propertize + "-" + 'face 'coq-button-face + 'mouse-face 'coq-button-face-pressed)) + +(defun coq-hypcross-folded-string() + (propertize + "+" + 'face 'coq-button-face + 'mouse-face 'coq-button-face-pressed)) + +;; hypcross is displayerd with a "-" when unfolded and a "+" when unfolded. +;; It is highlighted when hovered, is clickable and have a special +;; keymap (f toggles folding, h toggles highlighting...). +;; PC: using button faces of make-button makes the button larger than a +;; characters, which messes columns. So we use simple background colors in +;; coq-hyp...faces +(defun coq-make-hypcross-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hypcross t) + (overlay-put ov 'hyp-name h) + (overlay-put ov 'keymap coq-hypcross-map) + (overlay-put ov 'display (coq-hypcross-unfolded-string)) + ;(overlay-put ov 'face 'coq-button-face) + ;(overlay-put ov 'mouse-face 'coq-button-face-pressed) + ;(overlay-put ov 'width .6) + ;(overlay-put ov 'height -1) + (when (eq coq-hypcross-hovering-help t) + (overlay-put ov 'help-echo "mouse-3: unfold; mouse-2 copy name"))) + ov)) + +;; Once we have created the 3 overlays, each recieves a reference to the 2 +;; others. +(defun coq-hyp-overlay-build-cross-refs (hypnameov hypov crosshypov) + (overlay-put hypnameov 'hypcross-ov crosshypov) + (overlay-put hypov 'hypcross-ov crosshypov) + (overlay-put hypnameov 'hyp-ov hypov) + (overlay-put crosshypov 'hyp-ov hypov) + (overlay-put hypov 'hypname-ov hypnameov) + (overlay-put crosshypov 'hypname-ov hypnameov)) + +(defun coq-build-hyp-overlay (hyp-positions buf) + (let* ((names (car hyp-positions)) + (fstname (car names)) + (positions (cdr hyp-positions)) + (begcross (car positions)) + (beghypname (cadr positions)) + (endhypname (caddr positions)) + (beg (cadddr positions)) + (end (cadddr (cdr positions)))) + (let ((hypnameov (coq-make-hypname-overlay beghypname endhypname fstname buf)) + (hypov (coq-make-hyp-overlay beg end fstname buf)) + (crosshypov (coq-make-hypcross-overlay begcross (+ 1 begcross) fstname buf)) + res) + (coq-hyp-overlay-build-cross-refs hypnameov hypov crosshypov) + (mapc + (lambda (s) + (setq res + (cons + (cons (substring-no-properties s) + (cons hypov (cons hypnameov (cons crosshypov nil)) )) + res))) + names) + res))) + +(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)))) + 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 +for the whole hyp, only its name and the overlay for fold/unfold cross. +" + (coq-build-hyps-overlays (coq-detect-hyps-positions buf) buf)) + +(defun coq-find-hyp-overlay (h) + (cadr (assoc h coq-hyps-positions))) ;;;;;;;;;;;;;; Highlighting hypothesis ;;;;;;;; ;; Feature: highlighting of hyptohesis that remains when the cript is played @@ -1447,14 +1493,8 @@ 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.") +(defvar coq-hypcross-hovering-help t + "Whether hyps fold cross pops up a help when hovered.") ;; We maintain a list of hypothesis names that must be highlighted at each ;; regeneration of goals buffer. @@ -1464,16 +1504,26 @@ 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) + +;; Default binding: clicking on the name of an hyp with button 3 folds it. +;; Click on it with button 2 copies the names at current point. +(when coq-hypname-map + (define-key coq-hypname-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) (define-key coq-hypname-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) +(defvar coq-hypcross-map (make-sparse-keymap) "Keymap for visible hypothesis") +;; Default binding: clicking on the cross to folds/unfold hyp. +;; Click on it with button 2 copies the names at current point. + +(when coq-hypname-map + (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hypcross-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 buffer is updated." - (let ((hyp-overlay (coq-find-or-create-hyp-overlay h))) + (let ((hyp-overlay (coq-find-hyp-overlay h))) (when hyp-overlay (overlay-put hyp-overlay 'face '(:background "lavender")) (overlay-put hyp-overlay 'invisible nil)))) @@ -1548,33 +1598,28 @@ See `coq-highlight-hyp'." (coq-unhighlight-hyp h) (coq-highlight-hyp h))) -(defun coq-highlight () - "Toggle the hiding status of hypothesis H whose name is at point. -See `coq-hide-hyp'." +(defun coq-toggle-highlight-hyp-at (pt) + "Toggle hiding the hypothesis at point." (interactive) - (coq-toggle-highlight-hyp - (substring-no-properties (coq-id-or-notation-at-point)))) - - -(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) + (let* ((ov + (or (car (coq-overlays-at pt 'hyp-name)) + ;; we may be between hypname and hyp, so skip backward to + ;; something meaningful + (save-excursion + (goto-char pt) + (search-backward-regexp "[^ :=]\\|\n") + (car (coq-overlays-at (point) 'hyp-name))))) + (hypname (and ov + (overlay-get ov 'hyp-name)))) + (when hypname + (if (member hypname coq-highlighted-hyps) + (coq-unhighlight-hyp hypname) + (coq-highlight-hyp hypname))))) + +(defun coq-toggle-highlight-hyp-at-point () + (interactive) + (coq-toggle-highlight-hyp-at (point))) -(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") @@ -1591,51 +1636,52 @@ See `coq-hide-hyp'." 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) + +(defun coq-toggle-fold-hyp-at (pt) "Toggle hiding the hypothesis at point." (interactive) - (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))) - -(defun coq-toggle-hide-hyp-at-mouse (event) + (let* ((ov (car (coq-overlays-at pt 'hyp-name))) + (hypname (and ov (overlay-get ov 'hyp-name)))) + (when hypname + (if (member hypname coq-hidden-hyps) + (coq-unfold-hyp hypname) + (coq-fold-hyp hypname))))) + +(defun coq-toggle-fold-hyp-at-point () + (interactive) + (coq-toggle-fold-hyp-at (point))) + +(defun coq-toggle-fold-hyp-at-mouse (event) "Toggle hiding the hypothesis at mouse click. Used on hyptohesis overlays in goals buffer mainly." (interactive "e") (save-excursion (with-current-buffer proof-goals-buffer - (save-excursion (coq-toggle-hide-hyp-at (posn-point (event-start event))))))) + (save-excursion (coq-toggle-fold-hyp-at (posn-point (event-start event))))))) (defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden hypothesis") -;; Ddefault binding: clicking on a hidden hyp with button 3 unhides it, with +;; Ddefault binding: clicking on a hidden hyp with button 3 unfolds 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) + (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-fold-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 - (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 " : ........")))))) + (let* ((lgthhyp (- (overlay-end hyp-overlay) (overlay-start hyp-overlay))) + (prefx (make-string (min 8 lgthhyp) ?.)) + (hypcross-ov (overlay-get hyp-overlay 'hypcross-ov))) (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; mouse-2 copy name") - (overlay-put hyp-overlay 'hyp-name h) - (overlay-put hyp-overlay 'keymap coq-hidden-hyp-map))) + prefx ;(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: unfold; mouse-2 copy name") + (overlay-put hyp-overlay 'hyp-name h) + (overlay-put hyp-overlay 'keymap coq-hidden-hyp-map) + (overlay-put hypcross-ov 'display (coq-hypcross-folded-string))))) (defun coq-configure-hyp-overlay-visible (hyp-overlay h) (when hyp-overlay @@ -1643,89 +1689,76 @@ Used on hyptohesis overlays in goals buffer mainly." (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))) + (overlay-put hyp-overlay 'keymap nil) + (overlay-put (overlay-get hyp-overlay 'hypcross-ov) 'display (coq-hypcross-unfolded-string)))) -(defun coq-hide-hyp-aux (h) - "Hide hypothesis H's type from the context temporarily. +(defun coq-fold-hyp-aux (h) + "Fold hypothesis H's type from the context temporarily. 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 +buffer is changed, consider using `coq-fold-hyp' if you want the hiding to be maintain when scripting/undoing." - (let ((hyp-overlay (coq-find-or-create-hyp-overlay h))) + (let ((hyp-overlay (coq-find-hyp-overlay 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. +(defun coq-fold-hyp (h) + "Fold hypothesis H's type from the context durably. (displays \".......\" instead). This function relies on variable coq-hyps-positions. The hiding maintained as the goals buffer is changed, thanks to a hook on `proof-shell-handle-delayed-output-hook', consider using -`coq-hide-hyp' if you want the hiding to be maintain when +`coq-fold-hyp' if you want the hiding to be maintain when scripting/undoing." (interactive) (unless (member h coq-hidden-hyps) (setq coq-hidden-hyps (cons h coq-hidden-hyps)) - (coq-hide-hyp-aux h))) + (coq-fold-hyp-aux h))) -(defun coq-unhide-hyp-aux (h) -"Unhide hypothesis H temporarily. -See `coq-hide-hyp-aux'." - (let ((hyp-overlay (coq-find-or-create-hyp-overlay h))) +(defun coq-unfold-hyp-aux (h) +"Unfold hypothesis H temporarily. +See `coq-fold-hyp-aux'." + (let ((hyp-overlay (coq-find-hyp-overlay h))) (coq-configure-hyp-overlay-visible hyp-overlay h))) -(defun coq-unhide-hyp (h) -"Unhide hypothesis H durably. -See `coq-hide-hyp'." +(defun coq-unfold-hyp (h) +"Unfold hypothesis H durably. +See `coq-fold-hyp'." (interactive) (when (member h coq-hidden-hyps) (setq coq-hidden-hyps (delete h coq-hidden-hyps)) - (coq-unhide-hyp-aux h))) + (coq-unfold-hyp-aux h))) -(defun coq-unhide-hyp-list (lh) - "Hide the type of hypothesis in LH temporarily. -See `coq-unhide-hyp-aux'." - (mapc 'coq-unhide-hyp-aux lh)) +(defun coq-unfold-hyp-list (lh) + "Fold the type of hypothesis in LH temporarily. +See `coq-unfold-hyp-aux'." + (mapc 'coq-unfold-hyp-aux lh)) -(defun coq-hide-hyp-list (lh) - "Hide the type of hypothesis in LH temporarily. -See `coq-hide-hyp-aux'." - (mapc 'coq-hide-hyp-aux lh)) +(defun coq-fold-hyp-list (lh) + "Fold the type of hypothesis in LH temporarily. +See `coq-fold-hyp-aux'." + (mapc 'coq-fold-hyp-aux lh)) -(defun coq-hide-hyps () - "Hide the type of hypothesis in LH durably. -See `coq-hide-hyp'." +(defun coq-fold-hyps () + "Fold the type of hypothesis in LH durably. +See `coq-fold-hyp'." (interactive) - (coq-hide-hyp-list coq-hidden-hyps)) + (coq-fold-hyp-list coq-hidden-hyps)) -(defun coq-unhide-hyps () - "Unhide the type of hypothesis in LH durably. -See `coq-unhide-hyp'." +(defun coq-unfold-hyps () + "Unfold the type of hypothesis in LH durably. +See `coq-unfold-hyp'." (interactive) - (coq-unhide-hyp-list coq-hidden-hyps) + (coq-unfold-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) +(defun coq-toggle-fold-hyp (h) "Toggle the hiding status of hypothesis H (asked interactively). -See `coq-hide-hyp'." - (interactive "sHypothesis to hide: ") +See `coq-fold-hyp'." + (interactive "sHypothesis to fold: ") (if (member h coq-hidden-hyps) - (coq-unhide-hyp h) - (coq-hide-hyp h))) - -(defun coq-toggle-hide-hyp-at-point () - "Toggle the hiding status of hypothesis H whose name is at point. -See `coq-hide-hyp'." - (interactive) - (coq-toggle-hide-hyp - (substring-no-properties (coq-id-or-notation-at-point)))) + (coq-unfold-hyp h) + (coq-fold-hyp h))) ;;;;;;; (proof-definvisible coq-PrintHint "Print Hint. ") @@ -2806,6 +2839,10 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-ask-adapt-printing-width-and-show) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?l)] 'coq-LocateConstant) (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 [?h] 'coq-toggle-highlight-hyp-at-point) +(define-key coq-goals-mode-map [?H] 'coq-unhighlight-selected-hyps) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check) @@ -3047,10 +3084,11 @@ number of hypothesis displayed, without hiding the goal" (proof-clean-buffer proof-goals-buffer)))) (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) + (lambda () + (setq coq-hyps-positions (coq-detect-hyps proof-goals-buffer)) (coq-highlight-selected-hyps) - (coq-hide-hyps))) + (coq-fold-hyps) + )) -- cgit v1.2.3