added ident_with;
authorwenzelm
Sun, 22 May 2005 16:51:17 +0200
changeset 16029 070ed43b86f8
parent 16028 a2c790d145ba
child 16030 bbfb2f1378b3
added ident_with;
src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Sun May 22 16:51:16 2005 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Sun May 22 16:51:17 2005 +0200
@@ -19,6 +19,7 @@
   val pos_of: token -> string
   val is_kind: token_kind -> token -> bool
   val keyword_with: (string -> bool) -> token -> bool
+  val ident_with: (string -> bool) -> token -> bool
   val name_of: token -> string
   val is_proper: token -> bool
   val is_semicolon: token -> bool
@@ -110,6 +111,9 @@
 fun keyword_with pred (Token (_, (Keyword, x))) = pred x
   | keyword_with _ _ = false;
 
+fun ident_with pred (Token (_, (Ident, x))) = pred x
+  | ident_with _ _ = false;
+
 fun is_proper (Token (_, (Space, _))) = false
   | is_proper (Token (_, (Comment, _))) = false
   | is_proper _ = true;