diff options
| author | Hugo Herbelin | 2019-05-08 12:53:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:18 +0200 |
| commit | c6e2e57b8211dfc5bdaaa02592f8ae8bbad1d770 (patch) | |
| tree | 09dfadf393b79193104a9cd15990a6e5d9b78e8b /toplevel | |
| parent | ae7fc8bc74289bd8a1eca48c8ca8ecf923888285 (diff) | |
Toplevel: structuring source code.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ccompile.ml | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index e6255a947e..605db74836 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -20,6 +20,16 @@ let fatal_error msg = (******************************************************************************) (* Interactive Load File Simulation *) (******************************************************************************) + +let load_init_file opts ~state = + if opts.load_rcfile then + Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> + Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () + else begin + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + state + end + let load_vernacular opts ~state = List.fold_left (fun state (f_in, echo) -> @@ -32,16 +42,9 @@ let load_vernacular opts ~state = ) state (List.rev opts.load_vernacular_list) let load_init_vernaculars opts ~state = - let state = - if opts.load_rcfile then - Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> - Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () - else begin - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - state - end in - - load_vernacular opts ~state + let state = load_init_file opts ~state in + let state = load_vernacular opts ~state in + state (******************************************************************************) (* File Compilation *) |
