# HG changeset patch
# User wenzelm
# Date 1284756127 -7200
# Node ID d9cf3f83331861803dfe289c50cf6b240f2a29b7
# Parent  fce2202892c495eac2cfffeb7c55484d60db052b
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;

diff -r fce2202892c4 -r d9cf3f833318 src/Pure/ML/ml_syntax.ML
--- 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 "@")