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