tuned;

--- 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))
     }