# HG changeset patch
# User wenzelm
# Date 896123600 -7200
# Node ID 4ebdea55645719b6acfc0251df88540892decf4e
# Parent  ad2acb8d2db4495d914770285bc8b3c00e4381fa
added recover, source;

diff -r ad2acb8d2db4 -r 4ebdea556457 src/Pure/Syntax/symbol.ML
--- a/src/Pure/Syntax/symbol.ML	Mon May 25 21:12:46 1998 +0200
+++ b/src/Pure/Syntax/symbol.ML	Mon May 25 21:13:20 1998 +0200
@@ -24,6 +24,8 @@
   val explode: string -> symbol list
   val input: string -> string
   val output: string -> string
+  val source: bool -> (string, 'a) Source.source ->
+    (symbol, (string, 'a) Source.source) Source.source
 end;
 
 structure Symbol: SYMBOL =
@@ -210,6 +212,14 @@
   Scan.one not_eof;
 
 
+(* source *)
+
+val recover = Scan.any1 ((not o is_blank) andf not_eof);
+
+fun source do_recover src =
+  Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
+
+
 (* explode *)
 
 fun no_syms [] = true