src/Pure/Isar/token.ML
changeset 68729 3a02b424d5fb
parent 68298 2c3ce27cf4a8
child 68730 0bc491938780
     1.1 --- a/src/Pure/Isar/token.ML	Tue Jul 31 21:06:09 2018 +0200
     1.2 +++ b/src/Pure/Isar/token.ML	Tue Jul 31 21:11:24 2018 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4    val is_comment: T -> bool
     1.5    val is_informal_comment: T -> bool
     1.6    val is_formal_comment: T -> bool
     1.7 +  val is_ignored: T -> bool
     1.8    val is_begin_ignore: T -> bool
     1.9    val is_end_ignore: T -> bool
    1.10    val is_error: T -> bool
    1.11 @@ -227,6 +228,10 @@
    1.12  fun ident_with pred (Token (_, (Ident, x), _)) = pred x
    1.13    | ident_with _ _ = false;
    1.14  
    1.15 +fun is_ignored (Token (_, (Space, _), _)) = true
    1.16 +  | is_ignored (Token (_, (Comment NONE, _), _)) = true
    1.17 +  | is_ignored _ = false;
    1.18 +
    1.19  fun is_proper (Token (_, (Space, _), _)) = false
    1.20    | is_proper (Token (_, (Comment _, _), _)) = false
    1.21    | is_proper _ = true;