[location] Make location optional in Loc.located

This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.

We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.

The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.

2 files changed, 24 insertions, 24 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4641a2bc8..ab360f98d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -146,13 +146,10 @@ let print_highlight_location ib loc =
   highlight_lines
 
 let valid_buffer_loc ib loc =
-  not (Loc.is_ghost loc) &&
   let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
 
 (* This is specific to the toplevel *)
-let pr_loc loc =
-  if Loc.is_ghost loc then str"<unknown>"
-  else
+let pr_loc ?loc = Option.default (fun loc ->
     let fname = loc.Loc.fname in
     if CString.equal fname "" then
       Loc.(str"Toplevel input, characters " ++ int loc.bp ++
@@ -162,6 +159,7 @@ let pr_loc loc =
 	   str", line " ++ int loc.line_nb ++ str", characters " ++
 	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
 	   str":")
+  ) loc
 
 (* Toplevel error explanation. *)
 let error_info_for_buffer ?loc buf =
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 ->