(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module P = Printf module F = Format module C = Cps type ('a, 'b) item = Term of 'a * 'b | Context of 'a | Warn of string | String of string type ('a, 'b) specs = { pp_term : 'a -> F.formatter -> 'b -> unit; pp_context: F.formatter -> 'a -> unit } let level = ref 0 (* Internal functions *******************************************************) let std = F.std_formatter let err = F.err_formatter let init = let started = ref false in fun () -> if !started then () else begin P.printf "\n"; started := true end let pp_items frm st l items = let pp_item frm = function | Term (c, t) -> F.fprintf frm "%a@,%a" st.pp_context c (st.pp_term c) t | Context c -> F.fprintf frm "%a" st.pp_context c | Warn s -> F.fprintf frm "@,%s" s | String s -> F.fprintf frm "%s " s in let iter map frm l = List.iter (map frm) l in if !level >= l then F.fprintf frm "%a" (iter pp_item) items (* Interface functions ******************************************************) (* let warn msg = init (); P.printf " %s\n" msg; flush stdout *) let box () = F.fprintf std "@,@[%s" " "; F.pp_print_if_newline std () let unbox () = F.fprintf std "@]" let flush () = F.fprintf std "@]@." let box_err () = F.fprintf err "@[" 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 let items1 s = [Warn s] let ct_items1 s c t = [Warn s; Term (c, t)] let ct_items2 s1 c1 t1 s2 c2 t2 = [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)] let warn msg = F.fprintf std "@,%s" msg