From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 15 Apr 2004 12:52:24 +0000 (+0000)
Subject: added string_of_html_tag (plain text pretty printer for tags)
X-Git-Tag: dead_dir_walking~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57af26570f0925769d943e37a0c5f26acd8e3255;p=helm.git

added string_of_html_tag (plain text pretty printer for tags)
---

diff --git a/helm/ocaml/logger/helmLogger.ml b/helm/ocaml/logger/helmLogger.ml
index ce535d26c..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,9 +25,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
diff --git a/helm/ocaml/logger/helmLogger.mli b/helm/ocaml/logger/helmLogger.mli
index 6717e9410..633b5c3ec 100644
--- a/helm/ocaml/logger/helmLogger.mli
+++ b/helm/ocaml/logger/helmLogger.mli
@@ -10,6 +10,9 @@ type html_msg = [ `Error of html_tag | `Msg of html_tag ]
   (** html_msg to plain text converter *)
 val string_of_html_msg: html_msg -> string
 
+  (** html_tag to plain text converter *)
+val string_of_html_tag: html_tag -> string
+
   (** html_msg to html text converter *)
 val html_of_html_msg: html_msg -> string