--- a/src/Pure/Isar/parse.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Isar/parse.ML Sun Aug 26 21:46:50 2012 +0200
@@ -34,6 +34,7 @@
val verbatim: string parser
val sync: string parser
val eof: string parser
+ val command_name: string -> string parser
val keyword_with: (string -> bool) -> string parser
val keyword_ident_or_symbolic: string parser
val $$$ : string -> string parser
@@ -190,6 +191,11 @@
fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
+fun command_name x =
+ group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
+ (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
+ >> Token.content_of;
+
fun $$$ x =
group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
(keyword_with (fn y => x = y));