helm/gTopLevel/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