X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_proof_checking%2FcicLogger.ml;h=5921c61b0cf7c47ba17c938f685e963a7fac791f;hb=489ee5290cce2247291b8c5c53b98d493e7f6b99;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..5921c61b0 100644
--- a/helm/ocaml/cic_proof_checking/cicLogger.ml
+++ b/helm/ocaml/cic_proof_checking/cicLogger.ml
@@ -23,44 +23,40 @@
* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
type msg =
[ `Start_type_checking of UriManager.uri
| `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;;