Added a function that escapes XML characters in ppcmds.

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

2 files changed, 23 insertions, 0 deletions

diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 067c527002..20a97810e7 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -174,6 +174,27 @@ let qstring s = str ("\""^escape_string s^"\"")
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
+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.of_list
+        (List.map xmlescape (Stream.npeek max_int str)))
+    | x -> x
+
+
 (* 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 41ea9ca0f0..ab2804a53f 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -57,6 +57,8 @@ val qs : string -> std_ppcmds
 val quote : std_ppcmds -> std_ppcmds
 val strbrk : string -> std_ppcmds
 
+val xmlescape : ppcmd -> ppcmd
+
 (*s Boxing commands. *)
 
 val h : int -> std_ppcmds -> std_ppcmds