From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 18 Nov 2004 16:46:23 +0000 (+0000)
Subject: added a stateful logger which remember indentation level of recursive
X-Git-Tag: PRE_UNIVERSES~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e735b7ba95f1bafc1256280e96be888dd373a86;p=helm.git

added a stateful logger which remember indentation level of recursive
type checking
---

diff --git a/helm/ocaml/cic_proof_checking/cicLogger.ml b/helm/ocaml/cic_proof_checking/cicLogger.ml
index 6867b8b92..28d7a8c2c 100644
--- a/helm/ocaml/cic_proof_checking/cicLogger.ml
+++ b/helm/ocaml/cic_proof_checking/cicLogger.ml
@@ -29,16 +29,32 @@ type msg =
  | `Trusting of UriManager.uri
  ]
 
-let log =
+let log ?(level = 1) =
  let module U = UriManager in
     function
      | `Start_type_checking uri ->
-         HelmLogger.log (`Msg (`DIV (1, None, `T
+         HelmLogger.log (`Msg (`DIV (level, None, `T
           ("Type-Checking of " ^ (U.string_of_uri uri) ^ " started"))))
      | `Type_checking_completed uri ->
-         HelmLogger.log (`Msg (`DIV (1, Some "green", `T
+         HelmLogger.log (`Msg (`DIV (level, Some "green", `T
           ("Type-Checking of " ^ (U.string_of_uri uri) ^ " completed"))))
      | `Trusting uri ->
-         HelmLogger.log (`Msg (`DIV (1, Some "blue", `T
+         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
+
diff --git a/helm/ocaml/cic_proof_checking/cicLogger.mli b/helm/ocaml/cic_proof_checking/cicLogger.mli
index 848b30573..408bc8879 100644
--- a/helm/ocaml/cic_proof_checking/cicLogger.mli
+++ b/helm/ocaml/cic_proof_checking/cicLogger.mli
@@ -29,5 +29,14 @@ type msg =
  | `Trusting of UriManager.uri
  ]
 
+  (** Stateless logging. Each message is logged with indentation level 1 *)
 val log: msg -> unit
 
+  (** Stateful logging. Each `Start_type_checing message increase the
+  * indentation level by 1, each `Type_checking_completed message decrease it by
+  * the same amount. *)
+class logger:
+  object
+    method log: msg -> unit
+  end
+