src/Pure/Isar/outer_keyword.scala

 package isabelle
 
 
 object Outer_Keyword
 {
+  /* kinds */
+
   val MINOR = "minor"
   val CONTROL = "control"
   val DIAG = "diag"
   val THY_BEGIN = "theory-begin"
   val THY_SWITCH = "theory-switch"

   val PRF_DECL = "proof-decl"
   val PRF_ASM = "proof-asm"
   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)
   val heading = Set(THY_HEADING, PRF_HEADING)
   val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof1 =
     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
+      }
+  }
 }