X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2Flogger.ml;h=2fe8ac0a1bf93646252d383e3200b45a32be0942;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=efae1b19564c79ac5538e6a9f6b44e89547a566f;hpb=5b2c666a48028daeba3fe6692e6ad3e14cad0a42;p=helm.git

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) -> ())