From 054bed9c667344024077202cc4ca2fd4e77c4842 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 14 Jan 2020 15:38:50 +0100
Subject: Generic monadic indentation + specifically ext-lib / Compcert + doc.

This a generalization of PR#451 proposed by @Chobbes.

Since these syntax are not completely universal (and not builtin in
coq), the idea is to make the syntax customizable, especially to make
it possible to disable it.

NOTE: to make the Compcert syntax supported I had to refine the smie
lexer so that the ";" token was emitted as a fllback instead of ";
tactic".

NOTE2: I had to make the coq-user-token and coq-monadic-tokens be
tested ON THE RESULT of smie-coq-backward-token.
---
 CHANGES | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 4195c26a..2b686029 100644
--- a/CHANGES
+++ b/CHANGES
@@ -60,6 +60,22 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     
     The set of tokens can be seen in variable smie-grammar.
 
+*** Indentation of monadic notations.
+    Using the extensibility for indentation described above we provide
+    a way to define your own monadic operators using the
+    coq-smie-monadic-tokens in the same spirit as coq-smie-user-tokens
+    above.
+
+    By default two well established syntax are supported:
+
+       x <- e ;;
+       e
+
+     and 
+
+       do x <- e ;
+       e
+
 *** Clickable Hypothesis in goals buffer to copy/paste hyp names
 
     Clicking on a hyp name in goals buffer with button 2 copies its
-- 
cgit v1.2.3