# HG changeset patch
# User wenzelm
# Date 1495792305 -7200
# Node ID f3e4f9e6c485e818bbe3c947e91384980cb7f043
# Parent  db5e701b691a86ada7aa070f462c0a9785aa4cdc
more correct and complete output of control characters;

diff -r db5e701b691a -r f3e4f9e6c485 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Fri May 26 11:33:09 2017 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Fri May 26 11:51:45 2017 +0200
@@ -64,9 +64,12 @@
     (case ord s of
       34 => "\\\""
     | 92 => "\\\\"
+    | 7 => "\\a"
+    | 8 => "\\b"
     | 9 => "\\t"
     | 10 => "\\n"
-    | 11 => "\\f"
+    | 11 => "\\v"
+    | 12 => "\\f"
     | 13 => "\\r"
     | c =>
         if c < 32 then "\\^" ^ chr (c + 64)