(* ||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 : F.formatter -> 'a -> 'b -> unit; pp_context: F.formatter -> 'a -> unit } let level = ref 0 (* Internal functions *******************************************************) 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 = function | Term (c, t) -> st.pp_context frm c; st.pp_term frm c t | Context c -> st.pp_context frm c | Warn s -> F.fprintf frm "@[%s\n@]" s | String s -> F.fprintf frm "@[%s @]" s in if !level >= l then List.iter pp_item items (* Interface functions ******************************************************) let warn msg = init (); P.printf " %s\n" msg; flush stdout let log st l items = pp_items F.std_formatter st l items let error st items = pp_items F.err_formatter 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)]