From 31dda92a0bf190fd526e0a6d9502c197bdd08eb1 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 31 May 2018 21:48:40 +0200 Subject: Updated CHANGES about hiding and highlighting of hyps. --- CHANGES | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/CHANGES b/CHANGES index a1dce5bc..dad29f1b 100644 --- a/CHANGES +++ b/CHANGES @@ -60,6 +60,24 @@ 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 + + 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. + + M-x coq-toggle-hide-hyp + M-x coq-toggle-hide-hyp-at-point + + M-x coq-unhighlight-selected-hyps + + M-x coq-toggle-highlight-hyp + M-x coq-toggle-highlight-hyp-at-point + + Hypothesis cited in the response buffer after a "About" command + (C-c C-a C-a) will be highlighted. + +**** Hypothesis cited in the response buffer. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some -- cgit v1.2.3