# HG changeset patch
# User wenzelm
# Date 1217957347 -7200
# Node ID 31899d977a89eddbf9216e6fe20997a8bb43a0ea
# Parent  d4c5ddf98869161447866f8f738de691d05fd3e0
improved recover: also resync on symbol/comment/verbatim delimiters;

diff -r d4c5ddf98869 -r 31899d977a89 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Aug 05 19:29:06 2008 +0200
+++ b/src/Pure/General/symbol.ML	Tue Aug 05 19:29:07 2008 +0200
@@ -439,9 +439,15 @@
       (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
   Scan.one not_eof;
 
+val scan_resync =
+  Scan.one is_ascii_blank || $$ "\"" || $$ "`" || $$ "\\" ||
+  Scan.this_string "(*" || Scan.this_string "*)" ||
+  Scan.this_string "{*" || Scan.this_string "*}";
+
 val recover =
-  Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso s <> "`" andalso not_eof s)
-    >> (fn ss => malformed :: ss @ [end_malformed]);
+  Scan.this (explode "\\<") @@@
+    Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))
+  >> (fn ss => malformed :: ss @ [end_malformed]);
 
 in