ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_proof_checking / cicLogger.mli

diff --git a/helm/ocaml/cic_proof_checking/cicLogger.mli b/helm/ocaml/cic_proof_checking/cicLogger.mli
index 781abdef6e9a7b6275e14935df9336ddb3cf0a31..408bc8879998f0da714948589b3b441dc3425460 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicLogger.mli
+++ b/helm/ocaml/cic_proof_checking/cicLogger.mli
@@ -28,13 +28,15 @@ type msg =
  | `Type_checking_completed of UriManager.uri
  | `Trusting of UriManager.uri
  ]
-;;
 
-(* A callback that can be used to log to html *)
-val log_to_html : print_and_flush:(string -> unit) -> msg -> unit
+  (** Stateless logging. Each message is logged with indentation level 1 *)
+val log: msg -> unit
 
-(* The log function used. The default does nothing. *)
-val log_callback : (msg -> unit) ref
+  (** 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
 
-(* Log something via log_callback *)
-val log : msg -> unit