[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.

1 files changed, 5 insertions, 5 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 7f30a4acc0..bbc3e4bcb8 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -64,8 +64,8 @@ let is_known_option cmd = match cmd with
 (** Check whether a command is forbidden in the IDE *)
 
 let ide_cmd_checks ~id (loc,ast) =
-  let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
-  let warn msg = Feedback.(feedback ~id (Message (Warning, Some loc, strbrk msg))) in
+  let user_error s = CErrors.user_err ?loc ~hdr:"CoqIde" (str s) in
+  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
   if is_debug ast then
     user_error "Debug mode not available in the IDE";
   if is_known_option ast then
@@ -342,8 +342,8 @@ let about () = {
 let handle_exn (e, info) =
   let dummy = Stateid.dummy in
   let loc_of e = match Loc.get_loc e with
-    | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
-    | _ -> None in
+    | Some loc -> Some (Loc.unloc loc)
+    | _        -> None in
   let mk_msg () = CErrors.print ~info e in
   match e with
   | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
@@ -391,7 +391,7 @@ let quit = ref false
 let print_ast id =
   match Stm.get_ast id with
   | Some (loc, expr) -> begin
-      try  Texmacspp.tmpp ~loc expr
+      try  Texmacspp.tmpp ?loc expr
       with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
     end
   | None     -> Xml_datatype.PCData "ERROR"