X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Flib%2Flog.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Flib%2Flog.ml;h=0000000000000000000000000000000000000000;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=03e7b5b958a2b44dcca9a1571b7e12e948a60383;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git diff --git a/helm/software/lambda-delta/src/lib/log.ml b/helm/software/lambda-delta/src/lib/log.ml deleted file mode 100644 index 03e7b5b95..000000000 --- a/helm/software/lambda-delta/src/lib/log.ml +++ /dev/null @@ -1,95 +0,0 @@ -(* - ||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 - | LEnv of 'a - | Warn of string - | String of string - | Loc - -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 -} - -let level = ref 0 - -let loc = ref "unknown location" - -(* Internal functions *******************************************************) - -let clear () = - level := 0; loc := "unknown location" - -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 - | 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 - 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 et_items1 sc c st t = - [Warn sc; LEnv c; Warn st; Term (c, t)] - -let et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 = - let tl = match sc2, c2 with - | Some sc2, Some c2 -> et_items1 sc2 c2 st2 t2 - | None, None -> t_items1 st2 c1 t2 - | _ -> assert false - in - et_items1 sc1 c1 st1 t1 @ tl - -let et_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 = - let tl = match sc3, c3 with - | Some sc3, Some c3 -> et_items1 sc3 c3 st3 t3 - | None, None -> t_items1 st3 c1 t3 - | _ -> assert false - in - et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl - -let warn msg = F.fprintf std "@,%s" msg