aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-07 16:38:26 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-09 08:13:18 +0200
commit8a8caba36ea6b0fd67e026ee3833d3b5b25af56d (patch)
tree11e9dc8d525d3f6d61f815859b248ad03971f437 /lib/pp.ml
parent25b0a871bde109788492992f1cb417e7e163ffa3 (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 'lib/pp.ml')
0 files changed, 0 insertions, 0 deletions