1 files changed, 55 insertions, 22 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index d0989cfcc..d7ede1c2e 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
@@ -272,8 +271,17 @@ let read_sentence ~state input =
     (* TopErr.print_toplevel_parse_error reraise top_buffer; *)
     Exninfo.iraise reraise
 
+let extract_default_loc loc doc_id sid : Loc.t option =
+  match loc with
+  | Some _ -> loc
+  | None ->
+    try
+      let doc = Stm.get_doc doc_id in
+      Option.cata fst None Stm.(get_ast ~doc sid)
+    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  -> ()
@@ -290,8 +298,11 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   (* Re-enable when we switch back to feedback-based error printing *)
   | Message (Error,loc,msg) -> ()
   (* 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
   | 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.
@@ -341,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 =
@@ -383,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 =
@@ -399,3 +410,25 @@ let rec loop ~state =
                 str (Printexc.to_string any)) ++ spc () ++
          hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str "."));
       loop ~state
+
+(* Default toplevel loop *)
+let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
+
+let drop_args = ref None
+let loop ~opts ~state =
+  drop_args := Some opts;
+  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
+  if Dumpglob.dump () then begin
+    Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
+    Dumpglob.noglob ()
+  end;
+  let _ = loop ~state in
+  (* Initialise and launch the Ocaml toplevel *)
+  Coqinit.init_ocaml_path();
+  Mltop.ocaml_toploop();
+  (* We delete the feeder after the OCaml toploop has ended so users
+     of Drop can see the feedback. *)
+  Feedback.del_feeder tl_feed