-ui_logger.cmo: ui_logger.cmi
-ui_logger.cmx: ui_logger.cmi
+helmLogger.cmo: helmLogger.cmi
+helmLogger.cmx: helmLogger.cmi
PACKAGE = logger
-REQUIRES = helm-urimanager helm-cic_proof_checking lablgtk2
-INTERFACE_FILES = ui_logger.mli
-IMPLEMENTATION_FILES = ui_logger.ml
+REQUIRES =
+INTERFACE_FILES = \
+ helmLogger.mli
+IMPLEMENTATION_FILES = \
+ $(INTERFACE_FILES:%.mli=%.ml)
include ../Makefile.common
--- /dev/null
+
+open Printf
+
+(* HTML simulator (first in its kind) *)
+
+type html_tag =
+ [ `T of string
+ | `L of html_tag list
+ | `BR
+ | `DIV of int * string option * html_tag
+ ]
+
+type html_msg = [ `Error of html_tag | `Msg of html_tag ]
+
+type logger_fun = ?append_NL:bool -> html_msg -> unit
+
+let string_of_html_msg =
+ let rec aux indent =
+ let indent_str = String.make indent ' ' in
+ function
+ | `T s -> s
+ | `L msgs ->
+ String.concat ("\n" ^ indent_str) (List.map (aux indent) msgs)
+ | `BR -> "\n" ^ indent_str
+ | `DIV (local_indent, _, tag) ->
+ "\n" ^ indent_str ^ aux (indent + local_indent) tag
+ in
+ function
+ | `Error tag -> "Error: " ^ aux 0 tag
+ | `Msg tag -> aux 0 tag
+
+let html_of_html_msg =
+ let rec string_of_html_tag = function
+ | `T s -> s
+ | `L msgs ->
+ sprintf "<ul>\n%s\n</ul>"
+ (String.concat "\n"
+ (List.map
+ (fun msg -> sprintf "<li>%s</li>" (string_of_html_tag msg))
+ msgs))
+ | `BR -> "<br />\n"
+ | `DIV (indent, color, tag) ->
+ sprintf "<div style=\"%smargin-left:%fcm\">\n%s\n</div>"
+ (match color with None -> "" | Some color -> "color: " ^ color ^ "; ")
+ (float_of_int indent *. 0.5)
+ (string_of_html_tag tag)
+ in
+ function
+ | `Error tag -> "<b>Error: " ^ string_of_html_tag tag ^ "</b>"
+ | `Msg tag -> string_of_html_tag tag
+
+let log_callbacks = ref []
+
+let register_log_callback logger_fun =
+ log_callbacks := !log_callbacks @ [ logger_fun ]
+
+let log ?append_NL html_msg =
+ List.iter (fun logger_fun -> logger_fun ?append_NL html_msg) !log_callbacks
+
--- /dev/null
+
+type html_tag =
+ [ `BR
+ | `L of html_tag list
+ | `T of string
+ | `DIV of int * string option * html_tag (* indentation, color, tag *)
+ ]
+type html_msg = [ `Error of html_tag | `Msg of html_tag ]
+
+val string_of_html_msg: html_msg -> string
+val html_of_html_msg: html_msg -> string
+
+type logger_fun = ?append_NL:bool -> html_msg -> unit
+
+val register_log_callback: logger_fun -> unit
+
+val log: logger_fun
+
+++ /dev/null
-
-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 "\n" (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
-
-let html_of_html_msg =
- let rec string_of_html_tag = function
- | `T s -> s
- | `L msgs ->
- sprintf "<ul>\n%s\n</ul>"
- (String.concat "\n"
- (List.map
- (fun msg -> sprintf "<li>%s</li>" (string_of_html_tag msg))
- msgs))
- | `BR -> "<br />\n"
- in
- function
- | `Error tag -> "<b>Error: " ^ string_of_html_tag tag ^ "</b>"
- | `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
-
+++ /dev/null
-
-type html_tag = [ `BR | `L of html_tag list | `T of string ]
-type html_msg = [ `Error of html_tag | `Msg of html_tag ]
-
-val string_of_html_msg: html_msg -> string
-val html_of_html_msg: html_msg -> string
-
-class html_logger:
- ?width:int -> ?height:int -> ?packing:(GObj.widget -> unit) -> ?show:bool ->
- unit ->
- object
- (* in all methods below "append_NL" defaults to true *)
-
- (** log an HTML like message, see minimal markup above *)
- method log: ?append_NL:bool -> html_msg -> unit
-
- (** log a cic messages as degined in CicLogger *)
- method log_cic_msg: ?append_NL:bool -> CicLogger.msg -> unit
-
- end
-
projects / helm.git / commitdiff