# HG changeset patch
# User wenzelm
# Date 1191685609 -7200
# Node ID 9d057ff8e74c14e2d241b86ba86e0c620a885bc5
# Parent  bad2b2be1f245e4d2a375a6169d3167674c22b6d
added keyword_decl, command_decl;

diff -r bad2b2be1f24 -r 9d057ff8e74c src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Oct 06 16:50:09 2007 +0200
+++ b/src/Pure/General/markup.ML	Sat Oct 06 17:46:49 2007 +0200
@@ -43,6 +43,8 @@
   val termN: string val term: T
   val keywordN: string val keyword: string -> T
   val commandN: string val command: string -> T
+  val keyword_declN: string val keyword_decl: string -> T
+  val command_declN: string val command_decl: string -> string -> T
   val stringN: string val string: T
   val altstringN: string val altstring: T
   val verbatimN: string val verbatim: T
@@ -145,6 +147,11 @@
 val (keywordN, keyword) = markup_string "keyword" nameN;
 val (commandN, command) = markup_string "command" nameN;
 
+val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
+
+val command_declN = "command_decl";
+fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
+
 val (stringN, string) = markup "string";
 val (altstringN, altstring) = markup "altstring";
 val (verbatimN, verbatim) = markup "verbatim";