ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;

--- 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 "@")