X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicLogger.ml;h=28d7a8c2c86484337cd81c19f1c93c95bcf23517;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=9fc983fc7fec8e9588dd68efc7b28f48491a30f8;hpb=d70688ca1e1bcefc463d3397c6da77b40d055c85;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicLogger.ml b/helm/ocaml/cic_proof_checking/cicLogger.ml
index 9fc983fc7..28d7a8c2c 100644
--- a/helm/ocaml/cic_proof_checking/cicLogger.ml
+++ b/helm/ocaml/cic_proof_checking/cicLogger.ml
@@ -28,39 +28,33 @@ type msg =
  | `Type_checking_completed of UriManager.uri
  | `Trusting of UriManager.uri
  ]
-;;
 
-let log_to_html ~print_and_flush =
+let log ?(level = 1) =
  let module U = UriManager in
-  let indent = ref 0 in
-   let mkindent () = 
-    String.make !indent ' '
-   in
     function
      | `Start_type_checking uri ->
-         print_and_flush (
-          mkindent () ^
-          "<div style=\"margin-left: " ^
-          string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
-          "Type-Checking of " ^ (U.string_of_uri uri) ^ " started</div>\n"
-         ) ;
-         incr indent
+         HelmLogger.log (`Msg (`DIV (level, None, `T
+          ("Type-Checking of " ^ (U.string_of_uri uri) ^ " started"))))
      | `Type_checking_completed uri ->
-         decr indent ;
-         print_and_flush (
-           mkindent () ^
-          "<div style=\"color: green ; margin-left: " ^
-          string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
-          "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.</div>\n"
-         )
+         HelmLogger.log (`Msg (`DIV (level, Some "green", `T
+          ("Type-Checking of " ^ (U.string_of_uri uri) ^ " completed"))))
      | `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"
-         )
-;;
+         HelmLogger.log (`Msg (`DIV (level, Some "blue", `T
+          ((U.string_of_uri uri) ^ " is trusted."))))
+
+class logger =
+  object
+    val mutable level = 0 (* indentation level *)
+    method log (msg: msg) =
+      match msg with
+      | `Start_type_checking _ ->
+          level <- level + 1;
+          log ~level msg
+      | `Type_checking_completed _ ->
+          log ~level msg;
+          level <- level - 1;
+      | _ -> log ~level msg
+  end
+
+let log msg = log ~level:1 msg
 
-let log_callback = ref (function (_:msg) -> ())
-let log msg = !log_callback msg;;