From f1ca798c0e68dfb44630b73e2e1b262c8ec304b9 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 26 Oct 2017 14:37:51 +0200 Subject: Updating CHANGES with lexer extensibility. --- CHANGES | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 142d3d84..5b35e3d0 100644 --- a/CHANGES +++ b/CHANGES @@ -6,6 +6,8 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac * Changes of Proof General 4.4.1 from Proof General 4.4 +* Changes of Proof General 4.4.1 from Proof General 4.4 + ** Generic changes *** bug fixes @@ -38,6 +40,21 @@ 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. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some -- cgit v1.2.3