]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/lib/log.ml
aeef7f9ee3fb910724307fb3576283c05e99ffb9
[helm.git] / helm / software / helena / src / 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 S = String
13 module P = Printf
14
15 module U  = NUri
16
17 type ('a, 'b) item = Term of 'a * 'b
18                    | LEnv of 'a
19                    | Warn of string
20                    | Uri  of U.uri
21                    | Flush
22
23 type ('a, 'b) message = ('a, 'b) item list
24
25 type ('a, 'b) specs = {
26    pp_term: 'a -> out_channel -> 'b -> unit;
27    pp_lenv: out_channel -> 'a -> unit
28 }
29
30 (* Internal functions *******************************************************)
31
32 let std = stdout
33
34 let err = stderr
35
36 let pp_items och st l items =
37    let indent = S.make (l+l) ' ' in    
38    let pp_item och = function
39       | Term (c, t) -> P.fprintf och "%s%a\n" indent (st.pp_term c) t
40       | LEnv c      -> P.fprintf och "%s%a" indent st.pp_lenv c
41       | Warn s      -> P.fprintf och "%s%s\n" indent s
42       | Uri u       -> P.fprintf och "%s<%s>\n" indent (U.string_of_uri u)
43       | Flush       -> P.fprintf och "%!"
44    in
45    let iter map och l = List.iter (map och) l in
46    P.fprintf och "%a" (iter pp_item) items
47
48 (* Interface functions ******************************************************)
49
50 let log st l items = pp_items std st l items
51
52 let error st items = pp_items err st 0 items
53
54 let items1 s = [Warn s]
55
56 let t_items1 st c t =
57    [Warn st; Term (c, t)]
58
59 let et_items1 sc c st t =
60    [Warn sc; LEnv c; Warn st; Term (c, t)]
61
62 let et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 =
63    let tl = match sc2, c2 with
64       | Some sc2, Some c2 -> et_items1 sc2 c2 st2 t2
65       | None, None        -> t_items1 st2 c1 t2
66       | _                 -> assert false
67    in
68    et_items1 sc1 c1 st1 t1 @ tl  
69
70 let et_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 =
71    let tl = match sc3, c3 with
72       | Some sc3, Some c3 -> et_items1 sc3 c3 st3 t3
73       | None, None        -> t_items1 st3 c1 t3 
74       | _                 -> assert false
75    in   
76    et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl 
77
78 let specs = {
79    pp_term = (fun _ _ _ -> ());
80    pp_lenv = (fun _ _ -> ());
81 }
82
83 let warn level str = log specs level (items1 str)