From: Stefano Zacchiroli Date: Wed, 11 Feb 2004 11:56:15 +0000 (+0000) Subject: - split away gtk logger X-Git-Tag: V_0_3_0~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6118150362700ed8f44b82cf6164d1c52c6d48f;p=helm.git - split away gtk logger - renamed module to HelmLogger --- diff --git a/helm/ocaml/logger/.depend b/helm/ocaml/logger/.depend index fe62a32d5..28268d29e 100644 --- a/helm/ocaml/logger/.depend +++ b/helm/ocaml/logger/.depend @@ -1,2 +1,2 @@ -ui_logger.cmo: ui_logger.cmi -ui_logger.cmx: ui_logger.cmi +helmLogger.cmo: helmLogger.cmi +helmLogger.cmx: helmLogger.cmi diff --git a/helm/ocaml/logger/Makefile b/helm/ocaml/logger/Makefile index 9d0c0ffce..95b8c5510 100644 --- a/helm/ocaml/logger/Makefile +++ b/helm/ocaml/logger/Makefile @@ -1,8 +1,10 @@ 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 diff --git a/helm/ocaml/logger/helmLogger.ml b/helm/ocaml/logger/helmLogger.ml new file mode 100644 index 000000000..b4234b03c --- /dev/null +++ b/helm/ocaml/logger/helmLogger.ml @@ -0,0 +1,59 @@ + +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 "" + (String.concat "\n" + (List.map + (fun msg -> sprintf "
  • %s
    • " (string_of_html_tag msg)) + msgs)) + | `BR -> "
    \n" + | `DIV (indent, color, tag) -> + sprintf "
    \n%s\n
    " + (match color with None -> "" | Some color -> "color: " ^ color ^ "; ") + (float_of_int indent *. 0.5) + (string_of_html_tag tag) + in + function + | `Error tag -> "Error: " ^ string_of_html_tag tag ^ "" + | `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 + diff --git a/helm/ocaml/logger/helmLogger.mli b/helm/ocaml/logger/helmLogger.mli new file mode 100644 index 000000000..e31019e6e --- /dev/null +++ b/helm/ocaml/logger/helmLogger.mli @@ -0,0 +1,18 @@ + +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 + diff --git a/helm/ocaml/logger/ui_logger.ml b/helm/ocaml/logger/ui_logger.ml deleted file mode 100644 index 09e50e627..000000000 --- a/helm/ocaml/logger/ui_logger.ml +++ /dev/null @@ -1,101 +0,0 @@ - -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 "" - (String.concat "\n" - (List.map - (fun msg -> sprintf "
  • %s
    • " (string_of_html_tag msg)) - 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 - diff --git a/helm/ocaml/logger/ui_logger.mli b/helm/ocaml/logger/ui_logger.mli deleted file mode 100644 index d64603a4b..000000000 --- a/helm/ocaml/logger/ui_logger.mli +++ /dev/null @@ -1,21 +0,0 @@ - -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 -