get ride of console.out which is used for debuging and add position t…

…o message instead. add pos proof error and comd 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,7 +163,8 @@ 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 ->
@@ -172,13 +173,13 @@ let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result =
     let qres = Option.map (fun f -> f ()) qres in
     Tac_OK((Time.save (), ss, ps, finalize, prv, sym_pos), qres)
   with Fatal(Some p,m) ->
-    Console.out 3 (Color.red "%a") Pos.pp p;
-    Tac_Error(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