helm/software/lambda-delta/lib/log.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module P = Printf
  13 module F = Format
  14 module C = Cps
  15
  16 type ('a, 'b) item = Term of 'a * 'b
  17                    | Context of 'a
  18                    | Warn of string
  19                    | String of string
  20
  21 type ('a, 'b) specs = {
  22    pp_term   : 'a -> F.formatter -> 'b -> unit;
  23    pp_context: F.formatter -> 'a -> unit
  24 }
  25
  26 let level = ref 0
  27
  28 (* Internal functions *******************************************************)
  29
  30 let std = F.std_formatter
  31
  32 let err = F.err_formatter
  33
  34 let init =
  35    let started = ref false in
  36    fun () ->
  37       if !started then () else
  38       begin P.printf "\n"; started := true end
  39
  40 let pp_items frm st l items =
  41    let pp_item frm = function
  42       | Term (c, t) -> F.fprintf frm "%a@,%a" st.pp_context c (st.pp_term c) t
  43       | Context c   -> F.fprintf frm "%a" st.pp_context c
  44       | Warn s      -> F.fprintf frm "@,%s" s
  45       | String s    -> F.fprintf frm "%s " s
  46    in
  47    let iter map frm l = List.iter (map frm) l in
  48    if !level >= l then F.fprintf frm "%a" (iter pp_item) items
  49
  50 (* Interface functions ******************************************************)
  51
  52 (*
  53 let warn msg =
  54    init (); P.printf " %s\n" msg; flush stdout
  55 *)
  56 let box () = F.fprintf std "@,@[<v 2>%s" "  "; F.pp_print_if_newline std ()
  57
  58 let unbox () = F.fprintf std "@]"
  59
  60 let flush () = F.fprintf std "@]@."
  61
  62 let box_err () = F.fprintf err "@[<v>"
  63
  64 let flush_err () = F.fprintf err "@]@."
  65
  66 let log st l items = pp_items std st l items
  67
  68 let error st items = pp_items err st 0 items
  69
  70 let items1 s = [Warn s]
  71
  72 let ct_items1 s c t =
  73    [Warn s; Term (c, t)]
  74
  75 let ct_items2 s1 c1 t1 s2 c2 t2 =
  76    [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)]
  77
  78 let warn msg = F.fprintf std "@,%s" msg