Removed a unused function in Pp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16048 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 0 insertions, 27 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 71c72baa90..b899ef8231 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -188,31 +188,6 @@ let qstring s = str ("\""^escape_string s^"\"")
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
-let stream_map f s =
-  Stream.of_list (List.map f (Stream.npeek max_int s))
-
-let rec xmlescape ppcmd =
-  let rec escape what withwhat (len, str) =
-    try
-      let pos = String.index str what in
-      let (tlen, tail) =
-        escape what withwhat ((len - pos - 1),
-          (String.sub str (pos + 1) (len - pos - 1)))
-      in
-      (pos + tlen + String.length withwhat, String.sub str 0 pos ^ withwhat ^ tail)
-    with Not_found -> (len, str)
-  in
-  match ppcmd with
-    | Ppcmd_print (len, str) ->
-        Ppcmd_print (escape '"' """
-          (escape '<' "&lt;" (escape '&' "&amp;" (len, str))))
-      (* In XML we always print whole content so we can npeek the whole stream *)
-    | Ppcmd_box (x, str) ->
-      Ppcmd_box (x, stream_map xmlescape str)
-    | x -> x
-
-let xmlescape = stream_map xmlescape
-
 (* This flag tells if the last printed comment ends with a newline, to
   avoid empty lines *)
 let com_eol = ref false
diff --git a/lib/pp.mli b/lib/pp.mli
index 614023758d..b46115fd4a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -61,8 +61,6 @@ val qs : string -> std_ppcmds
 val quote : std_ppcmds -> std_ppcmds
 val strbrk : string -> std_ppcmds
 
-val xmlescape : std_ppcmds -> std_ppcmds
-
 (** {6 Boxing commands} *)
 
 val h : int -> std_ppcmds -> std_ppcmds