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 +++++++++++------------------- 1 file changed, 11 insertions(+), 19 deletions(-) (limited to 'CHANGES') 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. -- cgit v1.2.3