]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/logger/helmLogger.ml
- split away gtk logger
[helm.git] / helm / ocaml / logger / helmLogger.ml
1
2 open Printf
3
4 (* HTML simulator (first in its kind) *)
5
6 type html_tag =
7  [ `T of string
8  | `L of html_tag list 
9  | `BR
10  | `DIV of int * string option * html_tag
11  ]
12
13 type html_msg = [ `Error of html_tag | `Msg of html_tag ]
14
15 type logger_fun = ?append_NL:bool -> html_msg -> unit
16
17 let string_of_html_msg =
18   let rec aux indent =
19     let indent_str = String.make indent ' ' in
20     function
21     | `T s -> s
22     | `L msgs ->
23         String.concat ("\n" ^ indent_str) (List.map (aux indent) msgs)
24     | `BR -> "\n" ^ indent_str
25     | `DIV (local_indent, _, tag) ->
26         "\n" ^ indent_str ^ aux (indent + local_indent) tag
27   in
28   function
29     | `Error tag -> "Error: " ^ aux 0 tag
30     | `Msg tag -> aux 0 tag
31
32 let html_of_html_msg =
33   let rec string_of_html_tag = function
34     | `T s -> s
35     | `L msgs ->
36         sprintf "<ul>\n%s\n</ul>"
37           (String.concat "\n"
38             (List.map
39               (fun msg -> sprintf "<li>%s</li>" (string_of_html_tag msg))
40               msgs))
41     | `BR -> "<br />\n"
42     | `DIV (indent, color, tag) ->
43         sprintf "<div style=\"%smargin-left:%fcm\">\n%s\n</div>"
44           (match color with None -> "" | Some color -> "color: " ^ color ^ "; ")
45           (float_of_int indent *. 0.5)
46           (string_of_html_tag tag)
47   in
48   function
49     | `Error tag -> "<b>Error: " ^ string_of_html_tag tag ^ "</b>"
50     | `Msg tag -> string_of_html_tag tag
51
52 let log_callbacks = ref []
53
54 let register_log_callback logger_fun =
55   log_callbacks := !log_callbacks @ [ logger_fun ]
56
57 let log ?append_NL html_msg =
58   List.iter (fun logger_fun -> logger_fun ?append_NL html_msg) !log_callbacks
59