diff -r 5e57a6f24cdb -r c2c1e5944536 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Fri Aug 10 13:15:00 2012 +0200
+++ b/src/Pure/Isar/token.scala	Fri Aug 10 13:33:07 2012 +0200
@@ -28,6 +28,7 @@
     val VERBATIM = Value("verbatim text")
     val SPACE = Value("white space")
     val COMMENT = Value("comment text")
+    val ERROR = Value("bad input")
     val UNPARSED = Value("unparsed input")
   }
 
@@ -89,8 +90,15 @@
   def is_space: Boolean = kind == Token.Kind.SPACE
   def is_comment: Boolean = kind == Token.Kind.COMMENT
   def is_proper: Boolean = !is_space && !is_comment
+  def is_error: Boolean = kind == Token.Kind.ERROR
   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
 
+  def is_unfinished: Boolean = is_error &&
+   (source.startsWith("\"") ||
+    source.startsWith("`") ||
+    source.startsWith("{*") ||
+    source.startsWith("(*"))
+
   def is_begin: Boolean = is_keyword && source == "begin"
   def is_end: Boolean = is_keyword && source == "end"