scan: malformed result;

--- a/src/Pure/General/symbol.ML	Fri Dec 29 19:44:13 2000 +0100
+++ b/src/Pure/General/symbol.ML	Fri Dec 29 19:45:01 2000 +0100
@@ -13,6 +13,7 @@
   val sync: symbol
   val is_sync: symbol -> bool
   val not_sync: symbol -> bool
+  val malformed: symbol
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
@@ -61,6 +62,7 @@
 
 val space = " ";
 val sync = "\\<^sync>";
+val malformed = "\\<^malformed>";
 val eof = "";
 
 
@@ -280,7 +282,7 @@
 
 (* source *)
 
-val recover = Scan.any ((not o is_blank) andf not_eof);
+val recover = Scan.any ((not o is_blank) andf not_eof) >> K [malformed];
 
 fun source do_recover src =
   Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;