diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-08 22:51:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-09 08:13:18 +0200 |
| commit | b8ae2de5be242bbd1e34ec974627c81f99b16d23 (patch) | |
| tree | 6b6c2980e6aac60e53da6097dca7ae93db83d52e /parsing/cLexer.mli | |
| parent | 8a8caba36ea6b0fd67e026ee3833d3b5b25af56d (diff) | |
Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
Diffstat (limited to 'parsing/cLexer.mli')
| -rw-r--r-- | parsing/cLexer.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 2c05d6a95..3ad49eb74 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -36,6 +36,10 @@ val unfreeze : frozen_t -> unit val xml_output_comment : (string -> unit) Hook.t +(* Retrieve the comments lexed at a given location of the stream + currently being processeed *) +val extract_comments : int -> string list + val terminal : string -> Tok.t (** The lexer of Coq: *) |