diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 76 |
1 files changed, 50 insertions, 26 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d497789a6..38351a377 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -35,12 +35,16 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) (* Feedback received in the init stage, this is different as the STM will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) -let coqtop_init_feed = Coqloop.coqloop_feed +let coqtop_init_feed = Coqloop.coqloop_feed Topfmt.Initialization + +let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude + +let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile (* Default toplevel loop *) let console_toploop_run opts ~state = (* We initialize the console only if we run the toploop_run *) - let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in + let tl_feed = Feedback.add_feeder (Coqloop.coqloop_feed Topfmt.InteractiveLoop) in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () @@ -101,9 +105,16 @@ let load_vernacular opts ~state = else load_vernac s ) state (List.rev opts.load_vernacular_list) -let load_init_vernaculars opts ~state = - let state = if opts.load_rcfile then - Coqinit.load_rcfile ~rcfile:opts.rcfile ~state +let load_init_vernaculars cur_feeder opts ~state = + let state = + if opts.load_rcfile then begin + Feedback.del_feeder !cur_feeder; + let rc_feeder = Feedback.add_feeder coqtop_rcfile_feed in + let state = Coqinit.load_rcfile ~rcfile:opts.rcfile ~state in + Feedback.del_feeder rc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; + state + end else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -147,8 +158,8 @@ let fatal_error msg = flush_all (); exit 1 -let fatal_error_exn ?extra exn = - Topfmt.print_err_exn ?extra exn; +let fatal_error_exn exn = + Topfmt.print_err_exn Topfmt.Initialization exn; flush_all (); let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 @@ -194,7 +205,7 @@ let ensure_exists f = fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile opts ~echo ~f_in ~f_out = +let compile cur_feeder opts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in @@ -218,13 +229,18 @@ let compile opts ~echo ~f_in ~f_out = | None -> long_f_dot_v ^ "o" | Some f -> ensure_vo long_f_dot_v f in - let doc, sid = Stm.(new_doc + Feedback.del_feeder !cur_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; iload_path; require_libs; stm_options; }) in + Feedback.del_feeder doc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars opts ~state in + let state = load_init_vernaculars cur_feeder opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) @@ -265,13 +281,18 @@ let compile opts ~echo ~f_in ~f_out = async_proofs_tac_error_resilience = `None; } in - let doc, sid = Stm.(new_doc + Feedback.del_feeder !cur_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; iload_path; require_libs; stm_options; }) in + Feedback.del_feeder doc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars opts ~state in + let state = load_init_vernaculars cur_feeder opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in @@ -288,21 +309,21 @@ let compile opts ~echo ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile opts ~echo ~f_in ~f_out = +let compile cur_feeder opts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile opts ~echo ~f_in ~f_out; + compile cur_feeder opts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file opts (f_in, echo) = +let compile_file cur_feeder opts (f_in, echo) = if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile opts ~echo ~f_in ~f_out:None) f_in + (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out:None) f_in else - compile opts ~echo ~f_in ~f_out:None + compile cur_feeder opts ~echo ~f_in ~f_out:None -let compile_files opts = +let compile_files cur_feeder opts = let compile_list = List.rev opts.compile_list in - List.iter (compile_file opts) compile_list + List.iter (compile_file cur_feeder opts) compile_list (******************************************************************************) (* VIO Dispatching *) @@ -420,7 +441,7 @@ let init_toplevel arglist = CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - let init_feeder = Feedback.add_feeder coqtop_init_feed in + let init_feeder = ref (Feedback.add_feeder coqtop_init_feed) in Lib.init(); (* Coq's init process, phase 2: @@ -490,29 +511,32 @@ let init_toplevel arglist = let require_libs = require_libs opts in let stm_options = opts.stm_flags in let open Vernac.State in + Feedback.del_feeder !init_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in let doc, sid = Stm.(new_doc { doc_type = Interactive opts.toplevel_name; iload_path; require_libs; stm_options; }) in + Feedback.del_feeder doc_feeder; + init_feeder := Feedback.add_feeder coqtop_init_feed; let state = { doc; sid; proof = None; time = opts.time } in - Some (load_init_vernaculars opts ~state), opts + Some (load_init_vernaculars init_feeder opts ~state), opts (* Non interactive: we perform a sequence of compilation steps *) end else begin - compile_files opts; + compile_files init_feeder opts; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) do_vio opts; (* Allow the user to output an arbitrary state *) outputstate opts; None, opts - end; + end; with any -> flush_all(); - let extra = Some (str "Error during initialization: ") in - fatal_error_exn ?extra any + fatal_error_exn any end in - Feedback.del_feeder init_feeder; + Feedback.del_feeder !init_feeder; res let start () = |