From f832476404a29d7791c1a6d7970988d3b2e3ad9e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 18 Mar 2019 15:17:55 +0100
Subject: documentation

---
 gramlib/plexing.mli |  2 +-
 parsing/cLexer.mli  | 24 +++++++++++++++++++++++-
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 48722e01be..26443df026 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -14,7 +14,7 @@ type pattern = string * string option
 -      The first string is the constructor name (must start with
        an uppercase character). When it is empty, the second string
        is supposed to be a keyword.
--      The second string is the constructor parameter. Empty if it
+-      The second component is the constructor parameter. None if it
        has no parameter (corresponding to the 'wildcard' pattern).
 -      The way tokens patterns are interpreted to parse tokens is done
        by the lexer, function [tok_match] below. *)
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index b9f89f5052..6d5a621877 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -8,9 +8,31 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This should be functional but it is not due to the interface *)
+(** When one registers a keyword she can declare it starts a quotation.
+  In particular using QUOTATION("name:") in a grammar rule
+  declares "name:" as a keyword and the token QUOTATION is
+  matched whenever the keyword is followed by an identifier or a
+  parenthesized text. Eg
+
+    constr:x
+    string:[....]
+    ltac:(....)
+    ltac:{....}
+
+  The delimiter is made of 1 or more occurrences of the same parenthesis,
+  eg ((.....)) or [[[[....]]]]. The idea being that if the text happens to
+  contain the closing delimiter, one can make the delimiter longer and avoid
+  confusion (no escaping). Eg
+
+    string:[[ .. ']' .. ]]
+
+
+  Nesting the delimiter is allowed, eg ((..((...))..)) is OK.
+
+  Keywords don't need to end in ':' *)
 type starts_quotation = NoQuotation | Quotation
 
+(** This should be functional but it is not due to the interface *)
 val add_keyword : ?quotation:starts_quotation -> string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
-- 
cgit v1.2.3