Making explicit that errors happen in one of five executation phases.

The five phases are command line interpretation, initialization,
prelude loading, rcfile loading, and sentence interpretation (only the
two latters are located).

We then parameterize the feedback handler with the given execution
phase, so as to possibly annotate the message with information
pertaining to the phase.

4 files changed, 75 insertions, 52 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index a1a07fce8..17e848c5a 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -10,8 +10,8 @@
 
 let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s))
 
-let fatal_error ?extra exn =
-  Topfmt.print_err_exn ?extra exn;
+let fatal_error exn =
+  Topfmt.print_err_exn Topfmt.ParsingCommandLine exn;
   let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
   exit exit_code
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 63b8b538a..da9169514 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -150,29 +150,28 @@ let print_highlight_location ib loc =
 
 let valid_buffer_loc ib loc =
   let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
-
 (* Toplevel error explanation. *)
-let error_info_for_buffer ?loc buf =
-  Option.map (fun loc ->
+let error_info_for_buffer ?loc phase buf =
+  match loc with
+  | None -> Topfmt.pr_phase ?loc phase
+  | Some loc ->
       let fname = loc.Loc.fname in
-      let hl, loc =
         (* We are in the toplevel *)
-        match fname with
-        | Loc.ToplevelInput ->
-          let nloc = adjust_loc_buf buf loc in
-          if valid_buffer_loc buf loc then
-            (fnl () ++ print_highlight_location buf nloc, nloc)
-            (* in the toplevel, but not a valid buffer *)
-          else (mt (), nloc)
-          (* we are in batch mode, don't adjust location *)
-        | Loc.InFile _ ->
-           (mt (), loc)
-      in Topfmt.pr_loc loc ++ hl
-    ) loc
+      match fname with
+      | Loc.ToplevelInput ->
+        let nloc = adjust_loc_buf buf loc in
+        if valid_buffer_loc buf loc then
+          match Topfmt.pr_phase ~loc:nloc phase with
+          | None -> None
+          | Some hd -> Some (hd ++ fnl () ++ print_highlight_location buf nloc)
+        (* in the toplevel, but not a valid buffer *)
+        else Topfmt.pr_phase ~loc phase
+      (* we are in batch mode, don't adjust location *)
+      | Loc.InFile _ -> Topfmt.pr_phase ~loc phase
 
 (* Actual printing routine *)
-let print_error_for_buffer ?loc lvl msg buf =
-  let pre_hdr = error_info_for_buffer ?loc buf in
+let print_error_for_buffer ?loc phase lvl msg buf =
+  let pre_hdr = error_info_for_buffer ?loc phase buf in
   if !print_emacs
   then Topfmt.emacs_logger ?pre_hdr lvl msg
   else Topfmt.std_logger   ?pre_hdr lvl msg
@@ -282,7 +281,7 @@ let extract_default_loc loc doc_id sid : Loc.t option =
     with _ -> loc
 
 (** Coqloop Console feedback handler *)
-let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
+let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in
   match fb.contents with
   | Processed   -> ()
   | Incomplete  -> ()
@@ -301,9 +300,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *)
   | Message (Warning,loc,msg) ->
     let loc = extract_default_loc loc fb.doc_id fb.span_id in
-    TopErr.print_error_for_buffer ?loc Warning msg top_buffer
+    TopErr.print_error_for_buffer ?loc phase Warning msg top_buffer
   | Message (lvl,loc,msg) ->
-    TopErr.print_error_for_buffer ?loc lvl msg top_buffer
+    TopErr.print_error_for_buffer ?loc phase lvl msg top_buffer
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -353,7 +352,7 @@ let top_goal_print oldp newp =
     let (e, info) = CErrors.push exn in
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
-    TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
+    TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer
 
 (* Careful to keep this loop tail-rec *)
 let rec vernac_loop ~state =
@@ -395,7 +394,7 @@ let rec vernac_loop ~state =
     let (e, info) = CErrors.push any in
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
-    TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+    TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer;
     vernac_loop ~state
 
 let rec loop ~state =
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 39a9de4f8..6d9867fb9 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -30,7 +30,7 @@ val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
 (** Toplevel feedback printer. *)
-val coqloop_feed : Feedback.feedback -> unit
+val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit
 
 (** Main entry point of Coq: read and execute vernac commands. *)
 val loop : state:Vernac.State.t -> Vernac.State.t
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 () =