]> matita.cs.unibo.it Git - helm.git/commitdiff
added string_of_html_msg
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 30 Jan 2004 08:14:19 +0000 (08:14 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 30 Jan 2004 08:14:19 +0000 (08:14 +0000)
helm/ocaml/logger/ui_logger.ml
helm/ocaml/logger/ui_logger.mli

index a711f5d389a7bd507d7fbf997db781a135aef976..5be084efcae2cda075247f51e514a5f4ffc4f40a 100644 (file)
@@ -11,6 +11,16 @@ type html_tag =
 
 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 "" (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
+
 class html_logger ?width ?height ?packing ?show () =
  let scrolled_window = GBin.scrolled_window ?packing ?show () in
  let vadj = scrolled_window#vadjustment in
index 3c548550ffc183115901d63e1dba89d63686ed12..c66a226357f45fa872735a9146f5eabd1784a94b 100644 (file)
@@ -2,6 +2,8 @@
 type html_tag = [ `BR | `L of html_tag list | `T of string ]
 type html_msg = [ `Error of html_tag | `Msg of html_tag ]
 
+val string_of_html_msg: html_msg -> string
+
 class html_logger:
   ?width:int -> ?height:int -> ?packing:(GObj.widget -> unit) -> ?show:bool ->
     unit ->