src/Pure/Isar/token.scala

     val STRING = Value("string")
     val ALT_STRING = Value("back-quoted string")
     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")
   }
 
 
   /* token reader */

   def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
   def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
   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"
 
   def content: String =