--- a/src/Pure/Isar/token.ML Thu Aug 09 21:09:24 2012 +0200
+++ b/src/Pure/Isar/token.ML Thu Aug 09 22:31:04 2012 +0200
@@ -34,6 +34,7 @@
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
@@ -178,6 +179,9 @@
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 *)