*** empty log message ***

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

1 files changed, 12 insertions, 2 deletions

diff --git a/lib/pp.ml4 b/lib/pp.ml4
index d13044c9a0..0e4b6b05e0 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -101,15 +101,25 @@ let pifb () = [< 'Ppcmd_print_if_broken >]
 let ws n = [< 'Ppcmd_white_space n >]
 
 (* derived commands *)
+let mt () = [< >]
 let spc () = [< 'Ppcmd_print_break (1,0) >]
 let cut () = [< 'Ppcmd_print_break (0,0) >]
 let align () = [< 'Ppcmd_print_break (0,0) >]
 let int n = str (string_of_int n)
 let real r = str (string_of_float r)
 let bool b = str (string_of_bool b)
-let qstring s = str ("\""^(String.escaped s)^"\"")
+
+let rec escape_string s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '\\' || s.[i] == '"' then
+      let s' = String.sub s 0 i^"\\"^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+let qstring s = str ("\""^(escape_string s)^"\"")
 let qs = qstring
-let mt () = [< >]
 
 (* boxing commands *)
 let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]