# HG changeset patch
# User wenzelm
# Date 1262705343 -3600
# Node ID 92810c85262e5570f646d57c2e387848ca9db547
# Parent  bfe8d699873492e20bfa016d1a37f09392efdf16
more accurate scanning of bad input;

diff -r bfe8d6998734 -r 92810c85262e src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Tue Jan 05 15:45:32 2010 +0100
+++ b/src/Pure/General/scan.scala	Tue Jan 05 16:29:03 2010 +0100
@@ -283,17 +283,20 @@
       val string = quoted("\"") ^^ (x => Token(Token_Kind.STRING, x))
       val alt_string = quoted("`") ^^ (x => Token(Token_Kind.ALT_STRING, x))
 
-      val bad_input = many1(sym => !(symbols.is_blank(sym))) ^^
-        (x => Token(Token_Kind.BAD_INPUT, x))
+      val junk = many1(sym => !(symbols.is_blank(sym)))
+      val bad_delimiter =
+        ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token_Kind.BAD_INPUT, x + y) }
+      val bad = junk ^^ (x => Token(Token_Kind.BAD_INPUT, x))
 
 
       /* tokens */
 
       (space | (string | (alt_string | (verbatim ^^ (x => Token(Token_Kind.VERBATIM, x)) |
         comment ^^ (x => Token(Token_Kind.COMMENT, x)))))) |
+      bad_delimiter |
       ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
         keyword ^^ (x => Token(if (is_command(x)) Token_Kind.COMMAND else Token_Kind.KEYWORD, x))) |
-      bad_input
+      bad
     }
   }