Fix location of symbol in logs when the object is not found within a …

…tactic (#1078)

* Show the location in terminal when the unknown object exception is catched by the scope_term function

* add square brackets to location message when object is not found

* fix symbol location within tactic : move the location printing in the Lsp server side

* get ride of console.out which is used for debugging and add position to message instead. add pos proof error and command error too

src/common/pos.ml

@@ -99,18 +99,20 @@ let to_string : ?print_fname:bool -> pos -> string =
   else
     Printf.sprintf "%s%d:%d-%d" fname start_line start_col end_col
 
+let popt_to_string : ?print_fname:bool -> popt -> string =
+  fun ?(print_fname=true) pop ->
+  match pop with
+    | None -> "Unknown location "
+    | Some (p) -> to_string ~print_fname p ^ " "
+
 (** [pp ppf pos] prints the optional position [pos] on [ppf]. *)
 let pp : popt Lplib.Base.pp = fun ppf p ->
-  match p with
-  | None    -> string ppf "unknown location"
-  | Some(p) -> string ppf (to_string p)
+  string ppf (popt_to_string p)
 
 (** [short ppf pos] prints the optional position [pos] on [ppf]. *)
 let short : popt Lplib.Base.pp = fun ppf p ->
-  match p with
-  | None    -> string ppf "unknown location"
-  | Some(p) -> let print_fname=false in
-               string ppf (to_string ~print_fname p)
+  let print_fname=false in
+  string ppf (popt_to_string ~print_fname p)
 
 (** [map f loc] applies function [f] on the value of [loc] and keeps the
     position unchanged. *)

src/pure/pure.ml

@@ -163,20 +163,23 @@ let handle_command : state -> Command.t -> command_result =
         (t, ss, d.pdata_state, d.pdata_finalize, d.pdata_prv, d.pdata_sym_pos)
       in
         Cmd_Proof(ps, d.pdata_proof, d.pdata_sym_pos, d.pdata_end_pos)
-  with Fatal(p,m) -> Cmd_Error(p,m)
+  with Fatal(Some p,m) ->
+    Cmd_Error(Some p, Pos.popt_to_string p ^ m)
 
 let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result =
   fun (_, ss, ps, finalize, prv, sym_pos) tac n ->
   try
     let ps, qres = Handle.Tactic.handle ss sym_pos prv (ps, None) tac n in
     let qres = Option.map (fun f -> f ()) qres in
     Tac_OK((Time.save (), ss, ps, finalize, prv, sym_pos), qres)
-  with Fatal(p,m) -> Tac_Error(p,m)
+  with Fatal(Some p,m) ->
+    Tac_Error(Some p, Pos.popt_to_string p ^ m)
 
 let end_proof : proof_state -> command_result =
   fun (_, ss, ps, finalize, _, _) ->
   try Cmd_OK((Time.save (), finalize ss ps), None)
-  with Fatal(p,m) -> Cmd_Error(p,m)
+  with Fatal(Some p,m) ->
+    Cmd_Error(Some p, Pos.popt_to_string p ^ m)
 
 let get_symbols : state -> Term.sym Extra.StrMap.t =
   fun (_, ss) -> ss.in_scope