diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/Isar/token.ML Sat Apr 04 21:21:40 2015 +0200 @@ -43,10 +43,11 @@ val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool - val keyword_with: (string -> bool) -> T -> bool - val ident_with: (string -> bool) -> T -> bool val is_command: T -> bool val is_name: T -> bool + val keyword_with: (string -> bool) -> T -> bool + val is_private: T -> bool + val ident_with: (string -> bool) -> T -> bool val is_proper: T -> bool val is_improper: T -> bool val is_comment: T -> bool @@ -246,6 +247,8 @@ fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x | keyword_with _ _ = false; +val is_private = keyword_with (fn x => x = "private"); + fun ident_with pred (Token (_, (Ident, x), _)) = pred x | ident_with _ _ = false;