src/Pure/Isar/token.ML

   val is_proper: T -> bool
   val is_semicolon: T -> bool
   val is_comment: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
+  val is_error: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
   val source_of: T -> string
   val source_position_of: T -> Symbol_Pos.text * Position.T
   val content_of: T -> string

   | is_begin_ignore _ = false;
 
 fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
   | is_end_ignore _ = false;
 
+fun is_error (Token (_, (Error _, _), _)) = true
+  | is_error _ = false;
+
 
 (* blanks and newlines -- space tokens obey lines *)
 
 fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
   | is_blank _ = false;