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 ]
let string_of_html_msg =
let rec string_of_html_tag = function
| `T s -> s
| `L msgs -> String.concat "" (List.map string_of_html_tag msgs)
| `BR -> "\n"
in
function
| `Error tag -> "Error: " ^ string_of_html_tag tag
| `Msg tag -> string_of_html_tag 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