+
+open Printf
+
+(* HTML simulator (first in its kind) *)
+
+type html_tag =
+ [ `T of string
+ | `L of html_tag list
+ | `BR
+ ]
+
+type html_msg = [ `Error of html_tag | `Msg of html_tag ]
+
+class html_logger ~width ~height ~packing ~show () =
+ let scrolled_window = GBin.scrolled_window ~packing ~show () in
+ let vadj = scrolled_window#vadjustment in
+ let tv =
+ GText.view ~editable:false ~cursor_visible:false
+ ~width ~height ~packing:(scrolled_window#add) ()
+ in
+ let green =
+ tv#buffer#create_tag
+ [`FOREGROUND_SET true ;
+ `FOREGROUND_GDK
+ (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "green"))]
+ in
+ let red =
+ tv#buffer#create_tag
+ [`FOREGROUND_SET true ;
+ `FOREGROUND_GDK
+ (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "red"))]
+ in
+ object (self)
+
+ method log ?(append_NL = true)
+ (m : [`Msg of html_tag | `Error of html_tag])
+ =
+ let process_msg tags =
+ let rec aux =
+ function
+ `T s -> tv#buffer#insert ~tags s
+ | `L l -> List.iter aux l
+ | `BR -> tv#buffer#insert ~tags "\n"
+ in
+ aux
+ in
+ (match m with
+ | `Msg m -> process_msg [green] m
+ | `Error m -> process_msg [red] m);
+ if append_NL then
+ process_msg [] `BR;
+ vadj#set_value (vadj#upper)
+
+ val mutable cic_indent_level = 0
+
+ method log_cic_msg ?(append_NL = true) (cic_msg: CicLogger.msg) =
+ let get_indent () = String.make cic_indent_level ' ' in
+ let incr () = cic_indent_level <- cic_indent_level + 1 in
+ let decr () = cic_indent_level <- cic_indent_level - 1 in
+ let msg =
+ get_indent () ^
+ (match cic_msg with
+ | `Start_type_checking uri ->
+ incr ();
+ sprintf "Type checking of %s started" (UriManager.string_of_uri uri)
+ | `Type_checking_completed uri ->
+ decr ();
+ sprintf "Type checking of %s completed"
+ (UriManager.string_of_uri uri)
+ | `Trusting uri ->
+ sprintf "%s is trusted" (UriManager.string_of_uri uri))
+ in
+ self#log ~append_NL (`Msg (`T msg))
+
+ end
+