]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/logger/helmLogger.ml
Added a parameter (empty list) to load_notation.
[helm.git] / helm / ocaml / logger / helmLogger.ml
index ce535d26c1dfec76e89936d3eeb93d4488cf1c6c..c41674754fea271f1f9d6d38a3913089fa8bb599 100644 (file)
@@ -1,3 +1,4 @@
+(* $Id$ *)
 
 open Printf
 
@@ -14,7 +15,7 @@ type html_msg = [ `Error of html_tag | `Msg of html_tag ]
 
 type logger_fun = ?append_NL:bool -> html_msg -> unit
 
-let string_of_html_msg =
+let rec string_of_html_tag =
   let rec aux indent =
     let indent_str = String.make indent ' ' in
     function
@@ -25,9 +26,11 @@ let string_of_html_msg =
     | `DIV (local_indent, _, tag) ->
         "\n" ^ indent_str ^ aux (indent + local_indent) tag
   in
-  function
-    | `Error tag -> "Error: " ^ aux 0 tag
-    | `Msg tag -> aux 0 tag
+  aux 0
+
+let string_of_html_msg = function
+  | `Error tag -> "Error: " ^ string_of_html_tag tag
+  | `Msg tag -> string_of_html_tag tag
 
 let rec html_of_html_tag = function
   | `T s -> s