extractors for outer keyword declarations;

--- a/src/Pure/Isar/outer_keyword.ML	Wed May 05 23:55:29 2010 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Thu May 06 13:41:30 2010 +0200
@@ -146,7 +146,7 @@
 fun command_tags name = these (Option.map tags_of (command_keyword name));
 
 
-(* report *)
+(* reports *)
 
 val keyword_status_reportN = "keyword_status_report";
 

--- a/src/Pure/Isar/outer_keyword.scala	Wed May 05 23:55:29 2010 +0200
+++ b/src/Pure/Isar/outer_keyword.scala	Thu May 06 13:41:30 2010 +0200
@@ -9,6 +9,8 @@
 
 object Outer_Keyword
 {
+  /* kinds */
+
   val MINOR = "minor"
   val CONTROL = "control"
   val DIAG = "diag"
@@ -33,6 +35,9 @@
   val PRF_ASM_GOAL = "proof-asm-goal"
   val PRF_SCRIPT = "proof-script"
 
+
+  /* categories */
+
   val minor = Set(MINOR)
   val control = Set(CONTROL)
   val diag = Set(DIAG)
@@ -43,5 +48,25 @@
     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
+
+
+  /* reports */
+
+  object Keyword_Decl {
+    def unapply(msg: XML.Tree): Option[String] =
+      msg match {
+        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
+        case _ => None
+      }
+  }
+
+  object Command_Decl {
+    def unapply(msg: XML.Tree): Option[(String, String)] =
+      msg match {
+        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
+          Some((name, kind))
+        case _ => None
+      }
+  }
 }