# HG changeset patch
# User wenzelm
# Date 1218830242 -7200
# Node ID af1b39debf30389427ff48fb54ee143e3c059090
# Parent  4a419fd52f4426d3a1a5cdd37528722bb1b5c3cf
scan: proper recovery for escaped \\< symbols;

diff -r 4a419fd52f44 -r af1b39debf30 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Aug 15 21:56:07 2008 +0200
+++ b/src/Pure/General/symbol.ML	Fri Aug 15 21:57:22 2008 +0200
@@ -446,7 +446,7 @@
   Scan.this_string "{*" || Scan.this_string "*}";
 
 val recover =
-  Scan.this (explode "\\<") @@@
+  (Scan.this (explode "\\\\<") || Scan.this (explode "\\<")) @@@
     Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))
   >> (fn ss => malformed :: ss @ [end_malformed]);