]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/logger/helmLogger.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / logger / helmLogger.ml
index b4234b03cff9f0ec357f830d6bff6970de49878d..7a1e63483e76e6d319d54b0a5f46773fd925d69d 100644 (file)
@@ -14,7 +14,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,29 +25,31 @@ 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
+  | `L msgs ->
+      sprintf "<ul>\n%s\n</ul>"
+        (String.concat "\n"
+          (List.map
+            (fun msg -> sprintf "<li>%s</li>" (html_of_html_tag msg))
+            msgs))
+  | `BR -> "<br />\n"
+  | `DIV (indent, color, tag) ->
+      sprintf "<div style=\"%smargin-left:%fcm\">\n%s\n</div>"
+        (match color with None -> "" | Some color -> "color: " ^ color ^ "; ")
+        (float_of_int indent *. 0.5)
+        (html_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"
-    | `DIV (indent, color, tag) ->
-        sprintf "<div style=\"%smargin-left:%fcm\">\n%s\n</div>"
-          (match color with None -> "" | Some color -> "color: " ^ color ^ "; ")
-          (float_of_int indent *. 0.5)
-          (string_of_html_tag tag)
-  in
   function
-    | `Error tag -> "<b>Error: " ^ string_of_html_tag tag ^ "</b>"
-    | `Msg tag -> string_of_html_tag tag
+    | `Error tag -> "<b>Error: " ^ html_of_html_tag tag ^ "</b>"
+    | `Msg tag -> html_of_html_tag tag
 
 let log_callbacks = ref []