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 ':'

This should be functional but it is not due to the interface

When string is not an ident, returns a keyword.

Precondition: the input is a number (c.f. NumTok.t)

after loc Will advance a lexing location as the lexer does; this can be used to implement parsing resumption from a given position:

  let loc = Pcoq.Parsable.loc pa |> after in
  let str = Gramlib.Stream.of_string text in
  (* Stream.count being correct is critical for Coq's lexer *)
  Gramlib.Stream.njunk loc.ep str;
  let pa = Pcoq.Parsable.make ~loc str in
  (* ready to resume parsing *)