diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-07 16:38:26 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-09 08:13:18 +0200 |
commit | 8a8caba36ea6b0fd67e026ee3833d3b5b25af56d (patch) | |
tree | 11e9dc8d525d3f6d61f815859b248ad03971f437 /tactics/hints.mli | |
parent | 25b0a871bde109788492992f1cb417e7e163ffa3 (diff) |
Attaching all extra imperative components of the lexer/parser state to
the state of parsable streams, so that different lexing/parsing
processes can be started independently without conflicting.
Note however that these different lexing/parsing processes cannot be
run concurrently as they still work on the same piece of global memory
(i.e. calls to entry_parse should remain atomic). To go further, one
would typically need to be able to functionally pass the lexing state
to each call to the lexer.
Note that currently the beautifier is also running in the context of a
lexer/parser state (for the mapping of location to comments).
In particular, this fixes #5102 (parsing/lexing of bullets depending on
the lexing state which was global).
Diffstat (limited to 'tactics/hints.mli')
0 files changed, 0 insertions, 0 deletions