[parsing] add keyword-protected generic quotation

One can now register a quotation using a grammar rule with
QUOTATION("name:"). "name:" becomes a keyword and the token is
generated for name: followed by a 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.

The text inside the quotation is returned as a string (including the
parentheses), so that a third party parser can take care of it.

Keywords don't need to end in ':'.

1 files changed, 2 insertions, 0 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index c8a87e6cb6..f4c819eeb6 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -163,6 +163,8 @@ let is_token s = match string_split s with
 
 let rec parse_tokens = function
 | [GSymbString s] -> SymbToken ("", Some s)
+| [GSymbQualid ("QUOTATION", None); GSymbString s] ->
+    SymbToken ("QUOTATION", Some s)
 | [GSymbQualid ("SELF", None)] -> SymbSelf
 | [GSymbQualid ("NEXT", None)] -> SymbNext
 | [GSymbQualid ("LIST0", None); tkn] ->