From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 14 Jan 2004 17:59:01 +0000 (+0000)
Subject: moved to the logger module
X-Git-Tag: V_0_5_1_3~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fab0f4f352935ab462b6b58bd63cbf2812e3ef3e;p=helm.git

moved to the logger module
---

diff --git a/helm/gTopLevel/ui_logger.ml b/helm/gTopLevel/ui_logger.ml
deleted file mode 100644
index 019748613..000000000
--- a/helm/gTopLevel/ui_logger.ml
+++ /dev/null
@@ -1,76 +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 ]
-
-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/gTopLevel/ui_logger.mli b/helm/gTopLevel/ui_logger.mli
deleted file mode 100644
index a289e370e..000000000
--- a/helm/gTopLevel/ui_logger.mli
+++ /dev/null
@@ -1,19 +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 ]
-
-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
-