diff options
| author | herbelin | 2005-12-28 12:58:53 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-28 12:58:53 +0000 |
| commit | fd70bb7da02f4f1b86dd850f57387bac9966ef12 (patch) | |
| tree | ef2779f0ed0f8e1ac40cc07988a4f3a1d0792cd5 /lib | |
| parent | 370e3fda7526f70ff7a8ff2ae213c097ed9c1e0a (diff) | |
Remplacement Pp.qs par Pptactic.qsnew
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7751 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 91a99b5fbd..cd68a8dad4 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -122,17 +122,17 @@ let int n = str (string_of_int n) let real r = str (string_of_float r) let bool b = str (string_of_bool b) +(* In new syntax only double quote char is escaped by repeating it *) 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 + else if 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 qstring s = str ("\""^escape_string s^"\"") let qs = qstring (* boxing commands *) |