# HG changeset patch
# User wenzelm
# Date 894557108 -7200
# Node ID d492b2ab7351face982b158082b587ed5dc310a6
# Parent  a4301a63bf5c788b5c2f1f62cbd174f0208fb827
added 'space';

diff -r a4301a63bf5c -r d492b2ab7351 src/Pure/Syntax/symbol.ML
--- a/src/Pure/Syntax/symbol.ML	Thu May 07 13:02:23 1998 +0200
+++ b/src/Pure/Syntax/symbol.ML	Thu May 07 18:05:08 1998 +0200
@@ -2,12 +2,13 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Baroque characters.
+Generalized characters.
 *)
 
 signature SYMBOL =
 sig
   type symbol
+  val space: symbol
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
@@ -161,10 +162,12 @@
 
 type symbol = string;
 
+val space = " ";
+val eof = "";
+
 
 (* kinds *)
 
-val eof = "";
 fun is_eof s = s = eof;
 fun not_eof s = s <> eof;
 
@@ -213,7 +216,7 @@
 
 fun sym_explode str =
   let val chs = explode str in
-    if no_syms chs then chs	(*tune trivial case*)
+    if no_syms chs then chs     (*tune trivial case*)
     else map symbol (#1 (Scan.error (Scan.finite eof (Scan.repeat scan)) chs))
   end;