From 1725748691514dcb819df36da92b774c4f827dad Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 4 Jun 2018 21:29:45 +0200 Subject: Shorter CHANGES + smal fixes in hide/highlight hyps code. --- CHANGES | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'CHANGES') 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 -- cgit v1.2.3