diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 56 |
1 files changed, 56 insertions, 0 deletions
@@ -11,6 +11,7 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac *** bug fixes - Using query-replace (or replace-string) in the processed region doesn't wrongly jump to the first match anymore. + - cheat face (admit etc) now visible when locked. *** remove key-binding for proof-electric-terminator-toggle - The default key-binding for proof-electric-terminator-toggle @@ -18,6 +19,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac useful as we can expect users to configure electric-terminator once and for all. Hence the removal of this default key-binding. +*** add another (fallback) key-binding for proof-goto-point + - The default key-binding for proof-goto-point (C-c <C-return>) + was not available in TTYs. Now, this function can also be run + with "C-c RET", which happens to be automatically trigerred if + we type "C-c <C-return>" in a TTY. + ** Coq changes *** new menu Coq -> Auto Compilation for all background compilation options @@ -38,6 +45,55 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac compilation does not stop at the first error but rather continues as far as possible. +*** Limited extensibility for indentation + + Coq indentation mechanism is based on a fixed set of tokens and + precedence rules. Extensibility is now possible by adding new + syntax for a given token (no new token can be added). + + Typical example: if you define a infix operator xor you may + want to define it as a new syntax for token \/ in order to + have the indentation rules of or applied to xor. + + Use: + (setq coq-smie-user-tokens '(("xor" . "\\/"))) + + The set of tokens can be seen in variable smie-grammar. + +*** Clickable Hypothesis in goals buffer to copy/paste hyp names + + 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. + +*** Folding/unfolding hypothesis + + 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. "F" + unfolds all hypothesis. + + Hide/ unhide status remains when goal changes. + + +*** Highlighting of hypothesis + + You can highlight hypothesis in goals buffer on a per name + fashion. Hit "h" while on the hypothesis. "H" removes all + highlighting in the buffer. + + Highlighting status remains when goal changes. + + +**** 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: + + (setq coq-highlight-hyps-cited-in-response nil) + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some |