# HG changeset patch
# User wenzelm
# Date 1344516966 -7200
# Node ID 4b4ece802cb3a9a324e1c78e30ede055a07690c3
# Parent  a72f8ffecf318306271104056d9692b9a34e53ed
tuned;

diff -r a72f8ffecf31 -r 4b4ece802cb3 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Aug 09 14:37:43 2012 +0200
+++ b/src/Pure/General/scan.scala	Thu Aug 09 14:56:06 2012 +0200
@@ -373,13 +373,13 @@
 
       val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
 
-      val bad_delimiter =
+      val recover_delimited =
         (quoted_prefix("\"") | (quoted_prefix("`") | (verbatim_prefix | comment_prefix))) ^^
           (x => Token(Token.Kind.UNPARSED, x))
 
       val bad = one(_ => true) ^^ (x => Token(Token.Kind.UNPARSED, x))
 
-      space | (bad_delimiter |
+      space | (recover_delimited |
         (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
           command_keyword) | bad))
     }