moved here ui_logger from gTopLeve

diff --git a/helm/ocaml/logger/.cvsignore b/helm/ocaml/logger/.cvsignore
new file mode 100644 (file)
index 0000000..f5a6b2e
--- /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 (file)
index 0000000..fe62a32
--- /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 (file)
index 0000000..9d0c0ff
--- /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 (file)
index 0000000..0197486
--- /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 (file)
index 0000000..a289e37
--- /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
+