From 05a96edc1a298d5a6d92919e0b68f0377604387f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 14 Jan 2004 17:57:11 +0000 Subject: [PATCH] moved here ui_logger from gTopLeve --- helm/ocaml/logger/.cvsignore | 7 +++ helm/ocaml/logger/.depend | 2 + helm/ocaml/logger/Makefile | 8 ++++ helm/ocaml/logger/ui_logger.ml | 76 +++++++++++++++++++++++++++++++++ helm/ocaml/logger/ui_logger.mli | 19 +++++++++ 5 files changed, 112 insertions(+) create mode 100644 helm/ocaml/logger/.cvsignore create mode 100644 helm/ocaml/logger/.depend create mode 100644 helm/ocaml/logger/Makefile create mode 100644 helm/ocaml/logger/ui_logger.ml create mode 100644 helm/ocaml/logger/ui_logger.mli diff --git a/helm/ocaml/logger/.cvsignore b/helm/ocaml/logger/.cvsignore new file mode 100644 index 000000000..f5a6b2ed3 --- /dev/null +++ b/helm/ocaml/logger/.cvsignore @@ -0,0 +1,7 @@ +*.cma +*.cmo +*.cmx +*.cmi +*.cmxa +*.a +*.o diff --git a/helm/ocaml/logger/.depend b/helm/ocaml/logger/.depend new file mode 100644 index 000000000..fe62a32d5 --- /dev/null +++ b/helm/ocaml/logger/.depend @@ -0,0 +1,2 @@ +ui_logger.cmo: ui_logger.cmi +ui_logger.cmx: ui_logger.cmi diff --git a/helm/ocaml/logger/Makefile b/helm/ocaml/logger/Makefile new file mode 100644 index 000000000..9d0c0ffce --- /dev/null +++ b/helm/ocaml/logger/Makefile @@ -0,0 +1,8 @@ + +PACKAGE = logger +REQUIRES = helm-urimanager helm-cic_proof_checking lablgtk2 +INTERFACE_FILES = ui_logger.mli +IMPLEMENTATION_FILES = ui_logger.ml + +include ../Makefile.common + diff --git a/helm/ocaml/logger/ui_logger.ml b/helm/ocaml/logger/ui_logger.ml new file mode 100644 index 000000000..019748613 --- /dev/null +++ b/helm/ocaml/logger/ui_logger.ml @@ -0,0 +1,76 @@ + +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 + diff --git a/helm/ocaml/logger/ui_logger.mli b/helm/ocaml/logger/ui_logger.mli new file mode 100644 index 000000000..a289e370e --- /dev/null +++ b/helm/ocaml/logger/ui_logger.mli @@ -0,0 +1,19 @@ + +type html_tag = [ `BR | `L of html_tag list | `T of string ] +type html_msg = [ `Error of html_tag | `Msg of html_tag ] + +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 + -- 2.39.2