# HG changeset patch
# User wenzelm
# Date 978115501 -3600
# Node ID 794cd4d768b55cf9a7fc6d84c5a2b6dac822acf7
# Parent  01e2d857fb7837f1ee9d1c16ec63675f9361cbf9
scan: malformed result;

diff -r 01e2d857fb78 -r 794cd4d768b5 src/Pure/General/symbol.ML
--- 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;