# HG changeset patch # User wenzelm # Date 1197726775 -3600 # Node ID d30391cdd9d9725ce6878571962f157295ea68b9 # Parent 2fdb26d45184984a51e51922edb95742f293168e recover: not skip over "`"; diff -r 2fdb26d45184 -r d30391cdd9d9 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Sat Dec 15 14:35:50 2007 +0100 +++ b/src/Pure/General/symbol.ML Sat Dec 15 14:52:55 2007 +0100 @@ -426,7 +426,7 @@ Scan.one not_eof; val recover = - Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) + Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso s <> "`" andalso not_eof s) >> (fn ss => malformed :: ss @ [end_malformed]); in