--- a/src/Pure/General/markup.ML Sun May 30 13:47:12 2010 +0200
+++ b/src/Pure/General/markup.ML Sun May 30 14:14:30 2010 +0200
@@ -83,6 +83,7 @@
val keyword_declN: string val keyword_decl: string -> T
val command_declN: string val command_decl: string -> string -> T
val keywordN: string val keyword: string -> T
+ val operatorN: string val operator: T
val commandN: string val command: string -> T
val identN: string val ident: T
val stringN: string val string: T
@@ -271,6 +272,7 @@
fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
val (keywordN, keyword) = markup_string "keyword" nameN;
+val (operatorN, operator) = markup_elem "operator";
val (commandN, command) = markup_string "command" nameN;
val (identN, ident) = markup_elem "ident";
val (stringN, string) = markup_elem "string";