added some ASCII control symbols;
authorwenzelm
Thu, 03 Apr 2008 16:03:54 +0200
changeset 26524 63953bec4c98
parent 26523 18ccad3ecb2e
child 26525 14a56f013469
added some ASCII control symbols;
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);