1 files changed, 22 insertions, 20 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d6bcd2f15..3a67f4cbf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -21,11 +21,12 @@ open Vernacprop
 
 let checknav_simple (loc, cmd) =
   if is_navigation_vernac cmd && not (is_reset cmd) then
-    CErrors.user_err ~loc (str "Navigation commands forbidden in files.")
+    CErrors.user_err ?loc (str "Navigation commands forbidden in files.")
 
 let checknav_deep (loc, ast) =
   if is_deep_navigation_vernac ast then
-    CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.")
+    CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
+
 
 let disable_drop = function
   | Drop -> CErrors.error "Drop is forbidden."
@@ -33,10 +34,12 @@ let disable_drop = function
 
 (* Echo from a buffer based on position.
    XXX: Should move to utility file. *)
-let vernac_echo loc in_chan = let open Loc in
-  let len = loc.ep - loc.bp in
-  seek_in in_chan loc.bp;
-  Feedback.msg_notice @@ str @@ really_input_string in_chan len
+let vernac_echo ?loc in_chan = let open Loc in
+  Option.iter (fun loc ->
+      let len = loc.ep - loc.bp in
+      seek_in in_chan loc.bp;
+      Feedback.msg_notice @@ str @@ really_input_string in_chan len
+    ) loc
 
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
@@ -49,8 +52,8 @@ let set_formatter_translator ch =
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
-let pr_new_syntax_in_context loc chan_beautify ocom =
-  let loc = Loc.unloc loc in
+let pr_new_syntax_in_context ?loc chan_beautify ocom =
+  let loc = Option.cata Loc.unloc (0,0) loc in
   if !beautify_file then set_formatter_translator chan_beautify;
   let fs = States.freeze ~marshallable:`No in
   (* The content of this is not supposed to fail, but if ever *)
@@ -72,14 +75,14 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
     States.unfreeze fs;
     Format.set_formatter_out_channel stdout
 
-let pr_new_syntax po loc chan_beautify ocom =
+let pr_new_syntax ?loc po chan_beautify ocom =
   (* Reinstall the context of parsing which includes the bindings of comments to locations *)
-  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context chan_beautify loc) ocom
+  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc chan_beautify) ocom
 
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
-let pp_cmd_header loc com =
+let pp_cmd_header ?loc com =
   let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
   let noblank s = String.map (fun c ->
       match c with
@@ -87,7 +90,7 @@ let pp_cmd_header loc com =
 	| x -> x
       ) s
   in
-  let (start,stop) = Loc.unloc loc in
+  let (start,stop) = Option.cata Loc.unloc (0,0) loc in
   let safe_pr_vernac x =
     try Ppvernac.pr_vernac x
     with e -> str (Printexc.to_string e) in
@@ -98,9 +101,8 @@ let pp_cmd_header loc com =
 (* This is a special case where we assume we are in console batch mode
    and take control of the console.
  *)
-(* FIXME *)
-let print_cmd_header loc com =
-  Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com);
+let print_cmd_header ?loc com =
+  Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com);
   Format.pp_print_flush !Topfmt.std_ft ()
 
 let pr_open_cur_subgoals () =
@@ -141,14 +143,14 @@ let rec interp_vernac sid po (loc,com) =
     try
       (* The -time option is only supported from console-based
          clients due to the way it prints. *)
-      if !Flags.time then print_cmd_header loc com;
+      if !Flags.time then print_cmd_header ?loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
       let (reraise, info) = CErrors.push reraise in
       let info = begin
         match Loc.get_loc info with
-        | None   -> Loc.add_loc info loc
+        | None   -> Option.cata (Loc.add_loc info) info loc
         | Some _ -> info
       end in iraise (reraise, info)
 
@@ -177,8 +179,8 @@ and load_vernac verbosely sid file =
       in
 
       (* Printing of vernacs *)
-      if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast);
-      Option.iter (vernac_echo loc) in_echo;
+      if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
+      Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
       let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in
@@ -193,7 +195,7 @@ and load_vernac verbosely sid file =
       | Stm.End_of_input ->
           (* Is this called so comments at EOF are printed? *)
           if !beautify then
-            pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None;
+            pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None;
           if !Flags.beautify_file then close_out chan_beautify;
           !rsid
       | reraise ->