From: Stefano Zacchiroli 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 +