X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flogger%2FhelmLogger.ml;h=7a1e63483e76e6d319d54b0a5f46773fd925d69d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b4234b03cff9f0ec357f830d6bff6970de49878d;hpb=b6118150362700ed8f44b82cf6164d1c52c6d48f;p=helm.git diff --git a/helm/ocaml/logger/helmLogger.ml b/helm/ocaml/logger/helmLogger.ml index b4234b03c..7a1e63483 100644 --- a/helm/ocaml/logger/helmLogger.ml +++ b/helm/ocaml/logger/helmLogger.ml @@ -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 "" + (String.concat "\n" + (List.map + (fun msg -> sprintf "
  • %s
  • " (html_of_html_tag msg)) + msgs)) + | `BR -> "
    \n" + | `DIV (indent, color, tag) -> + sprintf "
    \n%s\n
    " + (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 "" - (String.concat "\n" - (List.map - (fun msg -> sprintf "
  • %s
  • " (string_of_html_tag msg)) - msgs)) - | `BR -> "
    \n" - | `DIV (indent, color, tag) -> - sprintf "
    \n%s\n
    " - (match color with None -> "" | Some color -> "color: " ^ color ^ "; ") - (float_of_int indent *. 0.5) - (string_of_html_tag tag) - in function - | `Error tag -> "Error: " ^ string_of_html_tag tag ^ "" - | `Msg tag -> string_of_html_tag tag + | `Error tag -> "Error: " ^ html_of_html_tag tag ^ "" + | `Msg tag -> html_of_html_tag tag let log_callbacks = ref []