scan: proper recovery for escaped \\< symbols;
authorwenzelm
Fri, 15 Aug 2008 21:57:22 +0200
changeset 27903af1b39debf30
parent 27902 4a419fd52f44
child 27904 343696007eca
scan: proper recovery for escaped \\< symbols;
src/Pure/General/symbol.ML
     1.1 --- a/src/Pure/General/symbol.ML	Fri Aug 15 21:56:07 2008 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Fri Aug 15 21:57:22 2008 +0200
     1.3 @@ -446,7 +446,7 @@
     1.4    Scan.this_string "{*" || Scan.this_string "*}";
     1.5  
     1.6  val recover =
     1.7 -  Scan.this (explode "\\<") @@@
     1.8 +  (Scan.this (explode "\\\\<") || Scan.this (explode "\\<")) @@@
     1.9      Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))
    1.10    >> (fn ss => malformed :: ss @ [end_malformed]);
    1.11