]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/logger/ui_logger.ml
- split away gtk logger
[helm.git] / helm / ocaml / logger / ui_logger.ml
diff --git a/helm/ocaml/logger/ui_logger.ml b/helm/ocaml/logger/ui_logger.ml
deleted file mode 100644 (file)
index 09e50e6..0000000
+++ /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 "<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
-