]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/logger/ui_logger.ml
split into two major parts:
[helm.git] / helm / ocaml / logger / ui_logger.ml
index 0197486135de534f9d8180426c627068aeadc630..09e50e6273a1071fdc75be1c8a22b2c397c72d03 100644 (file)
@@ -11,12 +11,37 @@ type html_tag =
 
 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 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) ()
+    ?width ?height ~packing:(scrolled_window#add) ()
  in
  let green =
   tv#buffer#create_tag