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