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