From 02b84a9050015890424581ccecd2cd761c0c5c01 Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA <alidrandco@yahoo.fr>
Date: Thu, 11 Apr 2024 15:45:10 +0200
Subject: [PATCH] get ride of console.out which is used for debuging and add
 position to message instead. add pos proof error and comd error too

---
 src/common/pos.ml | 16 +++++++++-------
 src/pure/pure.ml  |  9 +++++----
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/common/pos.ml b/src/common/pos.ml
index ff8cdc16a..4587ab0f7 100644
--- a/src/common/pos.ml
+++ b/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. *)
diff --git a/src/pure/pure.ml b/src/pure/pure.ml
index 49ba8098d..db8b33e9e 100644
--- a/src/pure/pure.ml
+++ b/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