]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/lib/log.ml
new message reporting system improves performance significatively
[helm.git] / helm / software / helena / src / lib / log.ml
index 480e3c1399ebfddf4be13a33f4fc0b1de3bfca30..aeef7f9ee3fb910724307fb3576283c05e99ffb9 100644 (file)
@@ -9,61 +9,44 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module S = String
 module P = Printf
-module F = Format
-module C = Cps
+
+module U  = NUri
 
 type ('a, 'b) item = Term of 'a * 'b
                    | LEnv of 'a
                    | Warn of string
-                  | String of string
-                   | Loc
+                   | Uri  of U.uri
+                   | Flush
 
 type ('a, 'b) message = ('a, 'b) item list
 
 type ('a, 'b) specs = {
-   pp_term: 'a -> F.formatter -> 'b -> unit;
-   pp_lenv: F.formatter -> 'a -> unit
+   pp_term: 'a -> out_channel -> 'b -> unit;
+   pp_lenv: out_channel -> 'a -> unit
 }
 
-let level = ref 0
-
-let loc = ref "unknown location"
-
 (* Internal functions *******************************************************)
 
-let clear () = 
-   level := 0; loc := "unknown location"
+let std = stdout
 
-let std = F.std_formatter
+let err = stderr
 
-let err = F.err_formatter
-
-let pp_items frm st l items =   
-   let pp_item frm = function
-      | Term (c, t) -> F.fprintf frm "@ %a%!" (st.pp_term c) t
-      | LEnv c      -> F.fprintf frm "%a%!" st.pp_lenv c
-      | Warn s      -> F.fprintf frm "@ %s%!" s
-      | String s    -> F.fprintf frm "%s " s
-      | Loc         -> F.fprintf frm " <%s>" !loc 
+let pp_items och st l items =
+   let indent = S.make (l+l) ' ' in    
+   let pp_item och = function
+      | Term (c, t) -> P.fprintf och "%s%a\n" indent (st.pp_term c) t
+      | LEnv c      -> P.fprintf och "%s%a" indent st.pp_lenv c
+      | Warn s      -> P.fprintf och "%s%s\n" indent s
+      | Uri u       -> P.fprintf och "%s<%s>\n" indent (U.string_of_uri u)
+      | Flush       -> P.fprintf och "%!"
    in
-   let iter map frm l = List.iter (map frm) l in
-   if !level >= l then F.fprintf frm "%a" (iter pp_item) items
+   let iter map och l = List.iter (map och) l in
+   P.fprintf och "%a" (iter pp_item) items
 
 (* Interface functions ******************************************************)
 
-let box l = 
-   if !level >= l then
-   begin F.fprintf std "@,@[<v 2>%s" "  "; F.pp_print_if_newline std () end
-
-let unbox l = if !level >= l then F.fprintf std "@]"
-
-let flush l = if !level >= l then F.fprintf std "@]@."
-
-let box_err () = F.fprintf err "@[<v>"
-
-let flush_err () = F.fprintf err "@]@."
-
 let log st l items = pp_items std st l items
 
 let error st items = pp_items err st 0 items
@@ -92,4 +75,9 @@ let et_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 =
    in   
    et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl 
 
-let warn msg = F.fprintf std "@,%s" msg
+let specs = {
+   pp_term = (fun _ _ _ -> ());
+   pp_lenv = (fun _ _ -> ());
+}
+
+let warn level str = log specs level (items1 str)