# HG changeset patch
# User wenzelm
# Date 1207231434 -7200
# Node ID 63953bec4c986f4b232b10b5699413bd13b0e320
# Parent  18ccad3ecb2e902f4430f2f36490fb79a400ca2b
added some ASCII control symbols;

diff -r 18ccad3ecb2e -r 63953bec4c98 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Apr 03 16:03:54 2008 +0200
+++ b/src/Pure/General/symbol.ML	Thu Apr 03 16:03:54 2008 +0200
@@ -8,6 +8,11 @@
 signature SYMBOL =
 sig
   type symbol
+  val SOH: symbol
+  val STX: symbol
+  val ETX: symbol
+  val EOT: symbol
+  val DEL: symbol
   val space: symbol
   val spaces: int -> string
   val is_char: symbol -> bool
@@ -80,7 +85,13 @@
 
 type symbol = string;
 
-val space = " ";
+val SOH = chr 1;
+val STX = chr 2;
+val ETX = chr 3;
+val EOT = chr 4;
+val DEL = chr 127;
+
+val space = chr 32;
 
 local
   val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);