diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-11 19:42:14 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 18:16:22 +0100 |
commit | 2a64471512ee7dcd6d6c65cd5a792344628616f0 (patch) | |
tree | 9c98439db32ece160fd08304bfc4f1b5a63584e2 /toplevel/vernac.mli | |
parent | 893f8a3a3c573ab6b11cc3938cc67ccdc1b6b4ea (diff) |
[toplevel] Move beautify to its own pass.
We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.
We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
Diffstat (limited to 'toplevel/vernac.mli')
-rw-r--r-- | toplevel/vernac.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index e909ada1e..ca825197b 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -26,5 +26,5 @@ val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.l (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) -val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> +val load_vernac : time:bool -> echo:bool -> check:bool -> interactive:bool -> state:State.t -> string -> State.t |