1.1 --- a/src/Pure/General/markup.ML	Sat Oct 06 16:50:09 2007 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sat Oct 06 17:46:49 2007 +0200
     1.3 @@ -43,6 +43,8 @@
     1.4    val termN: string val term: T
     1.5    val keywordN: string val keyword: string -> T
     1.6    val commandN: string val command: string -> T
     1.7 +  val keyword_declN: string val keyword_decl: string -> T
     1.8 +  val command_declN: string val command_decl: string -> string -> T
     1.9    val stringN: string val string: T
    1.10    val altstringN: string val altstring: T
    1.11    val verbatimN: string val verbatim: T
    1.12 @@ -145,6 +147,11 @@
    1.13  val (keywordN, keyword) = markup_string "keyword" nameN;
    1.14  val (commandN, command) = markup_string "command" nameN;
    1.15  
    1.16 +val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
    1.17 +
    1.18 +val command_declN = "command_decl";
    1.19 +fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
    1.20 +
    1.21  val (stringN, string) = markup "string";
    1.22  val (altstringN, altstring) = markup "altstring";
    1.23  val (verbatimN, verbatim) = markup "verbatim";