Merge PR #8950: [topfmt] Add phase attribute for toplevel printing.

6 files changed, 73 insertions, 81 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 7c28ef24d4..15411d55d0 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 let fatal_error exn =
-  Topfmt.print_err_exn Topfmt.ParsingCommandLine exn;
+  Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn 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 4630599229..5cf2157044 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -150,10 +150,11 @@ 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 phase buf =
+let error_info_for_buffer ?loc buf =
   match loc with
-  | None -> Topfmt.pr_phase ?loc phase
+  | None -> Topfmt.pr_phase ?loc ()
   | Some loc ->
       let fname = loc.Loc.fname in
         (* We are in the toplevel *)
@@ -161,17 +162,17 @@ let error_info_for_buffer ?loc phase buf =
       | 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
+          match Topfmt.pr_phase ~loc:nloc () 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
+        else Topfmt.pr_phase ~loc ()
       (* we are in batch mode, don't adjust location *)
-      | Loc.InFile _ -> Topfmt.pr_phase ~loc phase
+      | Loc.InFile _ -> Topfmt.pr_phase ~loc ()
 
 (* Actual printing routine *)
-let print_error_for_buffer ?loc phase lvl msg buf =
-  let pre_hdr = error_info_for_buffer ?loc phase buf in
+let print_error_for_buffer ?loc lvl msg buf =
+  let pre_hdr = error_info_for_buffer ?loc buf in
   if !print_emacs
   then Topfmt.emacs_logger ?pre_hdr lvl msg
   else Topfmt.std_logger   ?pre_hdr lvl msg
@@ -281,7 +282,7 @@ let extract_default_loc loc doc_id sid : Loc.t option =
     with _ -> loc
 
 (** Coqloop Console feedback handler *)
-let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in
+let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   match fb.contents with
   | Processed   -> ()
   | Incomplete  -> ()
@@ -300,9 +301,9 @@ let coqloop_feed phase (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 phase Warning msg top_buffer
+    TopErr.print_error_for_buffer ?loc Warning msg top_buffer
   | Message (lvl,loc,msg) ->
-    TopErr.print_error_for_buffer ?loc phase lvl msg top_buffer
+    TopErr.print_error_for_buffer ?loc 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.
@@ -362,7 +363,7 @@ let top_goal_print ~doc c 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 Topfmt.InteractiveLoop Feedback.Error msg top_buffer
+    TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
 
 (* Careful to keep this loop tail-rec *)
 let rec vernac_loop ~state =
@@ -404,7 +405,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 Topfmt.InteractiveLoop Feedback.Error msg top_buffer;
+    TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
     vernac_loop ~state
 
 let rec loop ~state =
@@ -430,7 +431,7 @@ let loop ~opts ~state =
   let open Coqargs in
   print_emacs := opts.print_emacs;
   (* We initialize the console only if we run the toploop_run *)
-  let tl_feed = Feedback.add_feeder (coqloop_feed Topfmt.InteractiveLoop) in
+  let tl_feed = Feedback.add_feeder coqloop_feed in
   if Dumpglob.dump () then begin
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index b11f13d3cb..7d03484412 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -27,7 +27,7 @@ val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
 (** Toplevel feedback printer. *)
-val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit
+val coqloop_feed : Feedback.feedback -> unit
 
 (** Last document seen after `Drop` *)
 val drop_last_doc : Vernac.State.t option ref
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 66469ff0b9..66af7f7cdf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -30,15 +30,6 @@ let print_header () =
   Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()
 
-(* 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 Topfmt.Initialization
-
-let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude
-
-let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile
-
 let memory_stat = ref false
 let print_memory_stat () =
   begin (* -m|--memory from the command-line *)
@@ -86,16 +77,11 @@ let load_vernacular opts ~state =
       else load_vernac s
     ) state (List.rev opts.load_vernacular_list)
 
-let load_init_vernaculars cur_feeder opts ~state =
+let load_init_vernaculars 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
+    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
@@ -140,7 +126,7 @@ let fatal_error msg =
   exit 1
 
 let fatal_error_exn exn =
-  Topfmt.print_err_exn Topfmt.Initialization exn;
+  Topfmt.(in_phase ~phase:Initialization print_err_exn exn);
   flush_all ();
   let exit_code =
     if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1
@@ -186,7 +172,7 @@ let ensure_exists f =
     fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
-let compile cur_feeder opts ~echo ~f_in ~f_out =
+let compile opts ~echo ~f_in ~f_out =
   let open Vernac.State in
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
@@ -210,18 +196,14 @@ let compile cur_feeder opts ~echo ~f_in ~f_out =
         | None -> long_f_dot_v ^ "o"
         | Some f -> ensure_vo long_f_dot_v f in
 
-      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 doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
+        Stm.new_doc
+        Stm.{ doc_type = VoDoc long_f_dot_vo;
+              iload_path; require_libs; stm_options;
+            } in
 
       let state = { doc; sid; proof = None; time = opts.time } in
-      let state = load_init_vernaculars cur_feeder opts ~state in
+      let state = load_init_vernaculars 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)
@@ -262,18 +244,14 @@ let compile cur_feeder opts ~echo ~f_in ~f_out =
           async_proofs_tac_error_resilience = `None;
         } in
 
-      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 doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
+        Stm.new_doc
+        Stm.{ doc_type = VioDoc long_f_dot_vio;
+              iload_path; require_libs; stm_options;
+            } in
 
       let state = { doc; sid; proof = None; time = opts.time } in
-      let state = load_init_vernaculars cur_feeder opts ~state in
+      let state = load_init_vernaculars 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
@@ -290,22 +268,22 @@ let compile cur_feeder 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 cur_feeder opts ~echo ~f_in ~f_out =
+let compile opts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile cur_feeder opts ~echo ~f_in ~f_out;
+  compile opts ~echo ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
-let compile_file cur_feeder opts (f_in, echo) =
+let compile_file opts (f_in, echo) =
   let f_out = opts.compilation_output_name in
   if !Flags.beautify then
     Flags.with_option Flags.beautify_file
-      (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out) f_in
+      (fun f_in -> compile opts ~echo ~f_in ~f_out) f_in
   else
-    compile cur_feeder opts ~echo ~f_in ~f_out
+    compile opts ~echo ~f_in ~f_out
 
-let compile_files cur_feeder opts =
+let compile_files opts =
   let compile_list = List.rev opts.compile_list in
-  List.iter (compile_file cur_feeder opts) compile_list
+  List.iter (compile_file opts) compile_list
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
@@ -414,7 +392,8 @@ let init_toplevel custom_init arglist =
   CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-  let init_feeder = ref (Feedback.add_feeder coqtop_init_feed) in
+  let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
+
   Lib.init();
 
   (* Coq's init process, phase 2:
@@ -485,20 +464,16 @@ let init_toplevel custom_init 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 doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
+            Stm.new_doc
+            Stm.{ doc_type = Interactive opts.toplevel_name;
+                  iload_path; require_libs; stm_options;
+                } in
         let state = { doc; sid; proof = None; time = opts.time } in
-        Some (load_init_vernaculars init_feeder opts ~state), opts
+        Some (load_init_vernaculars opts ~state), opts
       (* Non interactive: we perform a sequence of compilation steps *)
       end else begin
-        compile_files init_feeder opts;
+        compile_files opts;
         (* Careful this will modify the load-path and state so after
            this point some stuff may not be safe anymore. *)
         do_vio opts;
@@ -510,7 +485,7 @@ let init_toplevel custom_init arglist =
       flush_all();
       fatal_error_exn any
   end in
-  Feedback.del_feeder !init_feeder;
+  Feedback.del_feeder init_feeder;
   res
 
 type custom_toplevel = {
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index f842ca5ead..4bf76dae51 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -335,6 +335,20 @@ type execution_phase =
   | LoadingRcFile
   | InteractiveLoop
 
+let default_phase = ref InteractiveLoop
+
+let in_phase ~phase f x =
+  let op = !default_phase in
+  default_phase := phase;
+  try
+    let res = f x in
+    default_phase := op;
+    res
+  with exn ->
+    let iexn = Backtrace.add_backtrace exn in
+    default_phase := op;
+    Util.iraise iexn
+
 let pr_loc loc =
     let fname = loc.Loc.fname in
     match fname with
@@ -347,8 +361,8 @@ let pr_loc loc =
 	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
 	   str":")
 
-let pr_phase ?loc phase =
-  match phase, loc with
+let pr_phase ?loc () =
+  match !default_phase, loc with
   | LoadingRcFile, loc ->
      (* For when all errors go through feedback:
      str "While loading rcfile:" ++
@@ -363,10 +377,10 @@ let pr_phase ?loc phase =
      (* Note: interactive messages such as "foo is defined" are not located *)
      None
 
-let print_err_exn phase any =
+let print_err_exn any =
   let (e, info) = CErrors.push any in
   let loc = Loc.get_loc info in
-  let pre_hdr = pr_phase ?loc phase in
+  let pre_hdr = pr_phase ?loc () in
   let msg = CErrors.iprint (e, info) ++ fnl () in
   std_logger ?pre_hdr Feedback.Error msg
 
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 73dcb0064b..0ddf474970 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -61,9 +61,11 @@ type execution_phase =
   | LoadingRcFile
   | InteractiveLoop
 
+val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b
+
 val pr_loc : Loc.t -> Pp.t
-val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option
-val print_err_exn : execution_phase -> exn -> unit
+val pr_phase : ?loc:Loc.t -> unit -> Pp.t option
+val print_err_exn : exn -> unit
 
 (** [with_output_to_file file f x] executes [f x] with logging
     redirected to a file [file] *)