From 2b3ea4c27c875855413a6f4dd7453472684083df Mon Sep 17 00:00:00 2001
From: Abdelghani ALIDRA <alidrandco@yahoo.fr>
Date: Fri, 29 Mar 2024 15:21:23 +0100
Subject: [PATCH] add wanings to the print function

---
 src/handle/command.ml | 26 +++++++++++++++++++-------
 1 file changed, 19 insertions(+), 7 deletions(-)

diff --git a/src/handle/command.ml b/src/handle/command.ml
index 5ba340777..560ee5198 100644
--- a/src/handle/command.ml
+++ b/src/handle/command.ml
@@ -495,7 +495,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       let declpos = Pos.cat pos (Option.bind p_sym_typ (fun x -> x.pos)) in
       let pdata_finalize, printfct =
         match pe.elt with
-        | P_proof_abort -> wrn pe.pos "Proof aborted."; (fun ss _ps -> ss), fun() -> ()
+        | P_proof_abort ->
+          (fun ss _ps -> ss), fun() -> wrn pe.pos "Proof aborted.";
         | P_proof_admitted ->
           let pdata_finalize_fct ss ps =
             if finished ps then
@@ -512,16 +513,21 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
             in
             List.iter admit_goal ps.proof_goals;
             (* Add the symbol in the signature with a warning. *)
-            wrn pe.pos "Proof admitted.";
             (* Keep the definition only if the symbol is not opaque. *)
             let d =
               if opaq then None
-              else Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
+              else
+                Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
             in
             (* Add the symbol in the signature. *)
             fst (Sig_state.add_symbol
                    ss expo prop mstrat opaq p_sym_nam declpos a impl d) in
-                   pdata_finalize_fct, fun() -> Console.out 2 (Color.red "symbol %a : %a") uid id term a
+                     pdata_finalize_fct,
+                     fun() ->
+                        Console.out 2
+                        (Color.red "symbol %a : %a")
+                        uid id term a;
+                        wrn pe.pos "Proof admitted."
         | P_proof_end ->
           let pdata_finalize_fct ss ps =
             (* Check that the proof is indeed finished. *)
@@ -530,14 +536,20 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
             (* Keep the definition only if the symbol is not opaque. *)
             let d =
               if opaq then None
-              else Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
+              else
+                Option.map
+                  (fun m -> unfold (mk_Meta(m,[||])))
+                  ps.proof_term
             in
             (* Add the symbol in the signature. *)
             fst (Sig_state.add_symbol
                    ss expo prop mstrat opaq p_sym_nam declpos a impl d) in
-                   pdata_finalize_fct, fun() -> Console.out 2 (Color.red "symbol %a : %a") uid id term a
+                     pdata_finalize_fct,
+                     fun() ->
+                       Console.out 2
+                       (Color.red "symbol %a : %a")
+                       uid id term a
       in
-      
       (* Create the proof state. *)
       let pdata_state =
         let proof_goals = Proof.add_goals_of_problem p [] in