]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/logger/ui_logger.ml
new configure.ac with support for compile time configuration of termeditor/parser/...
[helm.git] / helm / ocaml / logger / ui_logger.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  ]
11
12 type html_msg = [ `Error of html_tag | `Msg of html_tag ]
13
14 class html_logger ~width ~height ~packing ~show () =
15  let scrolled_window = GBin.scrolled_window ~packing ~show () in
16  let vadj = scrolled_window#vadjustment in
17  let tv =
18    GText.view ~editable:false ~cursor_visible:false
19     ~width ~height ~packing:(scrolled_window#add) ()
20  in
21  let green =
22   tv#buffer#create_tag
23    [`FOREGROUND_SET true ;
24     `FOREGROUND_GDK
25      (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "green"))]
26  in
27  let red =
28   tv#buffer#create_tag
29    [`FOREGROUND_SET true ;
30     `FOREGROUND_GDK
31      (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "red"))]
32  in
33  object (self)
34
35    method log ?(append_NL = true)
36     (m : [`Msg of html_tag | `Error of html_tag])
37    =
38     let process_msg tags =
39      let rec aux =
40       function
41          `T s -> tv#buffer#insert ~tags s
42        | `L l -> List.iter aux l
43        | `BR -> tv#buffer#insert ~tags "\n"
44      in
45      aux
46     in
47     (match m with
48      | `Msg m -> process_msg [green] m
49      | `Error m -> process_msg [red] m);
50     if append_NL then
51       process_msg [] `BR;
52     vadj#set_value (vadj#upper)
53
54    val mutable cic_indent_level = 0
55
56    method log_cic_msg ?(append_NL = true) (cic_msg: CicLogger.msg) =
57      let get_indent () = String.make cic_indent_level ' ' in
58      let incr () = cic_indent_level <- cic_indent_level + 1 in
59      let decr () = cic_indent_level <- cic_indent_level - 1 in
60      let msg =
61        get_indent () ^
62        (match cic_msg with
63        | `Start_type_checking uri ->
64            incr ();
65            sprintf "Type checking of %s started" (UriManager.string_of_uri uri)
66        | `Type_checking_completed uri ->
67            decr ();
68            sprintf "Type checking of %s completed"
69             (UriManager.string_of_uri uri)
70        | `Trusting uri ->
71            sprintf "%s is trusted" (UriManager.string_of_uri uri))
72      in
73      self#log ~append_NL (`Msg (`T msg))
74
75   end
76