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