From ff8df07f6a3239b7f4f2718743f5d78b2419406a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 25 Oct 2002 15:59:37 +0000
Subject: [PATCH] The fact that an object is trusted is now logged.

---
 helm/ocaml/cic_proof_checking/cicEnvironment.ml | 2 +-
 helm/ocaml/cic_proof_checking/logger.ml         | 8 ++++++++
 helm/ocaml/cic_proof_checking/logger.mli        | 1 +
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 7ed957271..d48ff09bd 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -188,7 +188,7 @@ let is_type_checked uri =
     Cache.unchecked_to_frozen uri ;
     if !trust_obj uri then
      begin
-prerr_endline ("### " ^ UriManager.string_of_uri uri ^ " TRUSTED!!!") ;
+      Logger.log (`Trusting uri) ;
       set_type_checking_info uri ;
       trust_obj := always_trust ;
       CheckedObj (Cache.find_cooked uri)
diff --git a/helm/ocaml/cic_proof_checking/logger.ml b/helm/ocaml/cic_proof_checking/logger.ml
index efae1b195..2fe8ac0a1 100644
--- a/helm/ocaml/cic_proof_checking/logger.ml
+++ b/helm/ocaml/cic_proof_checking/logger.ml
@@ -26,6 +26,7 @@
 type msg =
  [ `Start_type_checking of UriManager.uri
  | `Type_checking_completed of UriManager.uri
+ | `Trusting of UriManager.uri
  ]
 ;;
 
@@ -52,6 +53,13 @@ let log_to_html ~print_and_flush =
           string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
           "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.</div>\n"
          )
+     | `Trusting uri ->
+         print_and_flush (
+           mkindent () ^
+          "<div style=\"color: blue ; margin-left: " ^
+          string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
+          (U.string_of_uri uri) ^ " is trusted.</div>\n"
+         )
 ;;
 
 let log_callback = ref (function (_:msg) -> ())
diff --git a/helm/ocaml/cic_proof_checking/logger.mli b/helm/ocaml/cic_proof_checking/logger.mli
index c5e74ec90..781abdef6 100644
--- a/helm/ocaml/cic_proof_checking/logger.mli
+++ b/helm/ocaml/cic_proof_checking/logger.mli
@@ -26,6 +26,7 @@
 type msg =
  [ `Start_type_checking of UriManager.uri
  | `Type_checking_completed of UriManager.uri
+ | `Trusting of UriManager.uri
  ]
 ;;
 
-- 
2.39.2