--- a/src/Pure/Isar/token.ML Tue Jul 31 21:06:09 2018 +0200
+++ b/src/Pure/Isar/token.ML Tue Jul 31 21:11:24 2018 +0200
@@ -47,6 +47,7 @@
val is_comment: T -> bool
val is_informal_comment: T -> bool
val is_formal_comment: T -> bool
+ val is_ignored: T -> bool
val is_begin_ignore: T -> bool
val is_end_ignore: T -> bool
val is_error: T -> bool
@@ -227,6 +228,10 @@
fun ident_with pred (Token (_, (Ident, x), _)) = pred x
| ident_with _ _ = false;
+fun is_ignored (Token (_, (Space, _), _)) = true
+ | is_ignored (Token (_, (Comment NONE, _), _)) = true
+ | is_ignored _ = false;
+
fun is_proper (Token (_, (Space, _), _)) = false
| is_proper (Token (_, (Comment _, _), _)) = false
| is_proper _ = true;