X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicLogger.ml;h=28d7a8c2c86484337cd81c19f1c93c95bcf23517;hb=0d0b78958d6198e157171b3590516666d568c85f;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 () ^
- "
" ^
- "Type-Checking of " ^ (U.string_of_uri uri) ^ " started
\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 () ^
- "" ^
- "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.
\n"
- )
+ HelmLogger.log (`Msg (`DIV (level, Some "green", `T
+ ("Type-Checking of " ^ (U.string_of_uri uri) ^ " completed"))))
| `Trusting uri ->
- print_and_flush (
- mkindent () ^
- "" ^
- (U.string_of_uri uri) ^ " is trusted.
\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;;