diff options
| author | Hugo Herbelin | 2019-05-08 13:02:56 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | 5f3777e9ca29493a242b66f92ba803fa5760a634 (patch) | |
| tree | 340d074f206fe3b38bbfbb8d630f96924032f253 | |
| parent | c6e2e57b8211dfc5bdaaa02592f8ae8bbad1d770 (diff) | |
Toplevel: structuring init_toplevel.
| -rw-r--r-- | toplevel/coqtop.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e43e6a8da4..170959f2e2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -257,8 +257,7 @@ type custom_toplevel = ; opts : Coqargs.t } - -let init_toploop opts = +let init_document opts = let iload_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.stm_flags in @@ -268,8 +267,12 @@ let init_toploop opts = { doc_type = Interactive opts.toplevel_name; iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None; time = opts.time } in - Ccompile.load_init_vernaculars opts ~state, opts + { doc; sid; proof = None; time = opts.time } + +let init_toploop opts = + let state = init_document opts in + let state = Ccompile.load_init_vernaculars opts ~state in + state let coqtop_init ~opts extra = init_color opts; @@ -297,7 +300,7 @@ let start_coq custom = prerr_endline "See -help for the list of supported options"; exit 1 end; - init_toploop opts + init_toploop opts, opts with any -> flush_all(); fatal_error_exn any in |