aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-11 19:42:14 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-28 18:16:22 +0100
commit2a64471512ee7dcd6d6c65cd5a792344628616f0 (patch)
tree9c98439db32ece160fd08304bfc4f1b5a63584e2 /toplevel/coqinit.ml
parent893f8a3a3c573ab6b11cc3938cc67ccdc1b6b4ea (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/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d8aaf3db8..6f461fd53 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -26,7 +26,7 @@ let load_rcfile ~rcfile ~time ~state =
match rcfile with
| Some rcfile ->
if CUnix.file_readable_p rcfile then
- Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state rcfile
+ Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile
else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
| None ->
try
@@ -37,7 +37,7 @@ let load_rcfile ~rcfile ~time ~state =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state inferedrc
+ Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc
with Not_found -> state
(*
Flags.if_verbose