(* ||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 | Loc type ('a, 'b) specs = { pp_term : 'a -> F.formatter -> 'b -> unit; pp_context: F.formatter -> 'a -> unit } let level = ref 0 let loc = ref 0 (* Internal functions *******************************************************) let std = F.std_formatter 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 | Context c -> F.fprintf frm "%a" st.pp_context c | Warn s -> F.fprintf frm "@,%s" s | String s -> F.fprintf frm "%s " s | Loc -> F.fprintf frm " (line %u)" !loc 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 box l = if !level >= l then begin F.fprintf std "@,@[%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 "@[" 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 t_items1 st c t = [Warn st; Term (c, t)] let ct_items1 sc c st t = [Warn sc; Context c; Warn st; Term (c, t)] let ct_items2 sc c st1 t1 st2 t2 = ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2)] let ct_items3 sc c st1 t1 st2 t2 st3 t3 = ct_items2 sc c st1 t1 st2 t2 @ [Warn st3; Term (c, t3)] let warn msg = F.fprintf std "@,%s" msg