changeset 39514 | d9cf3f833318 |
parent 37535 | 75de61a479e3 |
child 40626 | d86540f6ea0d |
--- a/src/Pure/ML/ml_syntax.ML Fri Sep 17 22:17:57 2010 +0200 +++ b/src/Pure/ML/ml_syntax.ML Fri Sep 17 22:42:07 2010 +0200 @@ -62,6 +62,9 @@ if not (Symbol.is_char s) then s else if s = "\"" then "\\\"" else if s = "\\" then "\\\\" + else if s = "\t" then "\\t" + else if s = "\n" then "\\n" + else if s = "\r" then "\\r" else let val c = ord s in if c < 32 then "\\^" ^ chr (c + ord "@")