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

     2.1 --- a/src/Pure/Isar/outer_keyword.scala	Wed May 05 23:55:29 2010 +0200
     2.2 +++ b/src/Pure/Isar/outer_keyword.scala	Thu May 06 13:41:30 2010 +0200
     2.3 @@ -9,6 +9,8 @@
     2.4  
     2.5  object Outer_Keyword
     2.6  {
     2.7 +  /* kinds */
     2.8 +
     2.9    val MINOR = "minor"
    2.10    val CONTROL = "control"
    2.11    val DIAG = "diag"
    2.12 @@ -33,6 +35,9 @@
    2.13    val PRF_ASM_GOAL = "proof-asm-goal"
    2.14    val PRF_SCRIPT = "proof-script"
    2.15  
    2.16 +
    2.17 +  /* categories */
    2.18 +
    2.19    val minor = Set(MINOR)
    2.20    val control = Set(CONTROL)
    2.21    val diag = Set(DIAG)
    2.22 @@ -43,5 +48,25 @@
    2.23      Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    2.24    val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    2.25    val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    2.26 +
    2.27 +
    2.28 +  /* reports */
    2.29 +
    2.30 +  object Keyword_Decl {
    2.31 +    def unapply(msg: XML.Tree): Option[String] =
    2.32 +      msg match {
    2.33 +        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
    2.34 +        case _ => None
    2.35 +      }
    2.36 +  }
    2.37 +
    2.38 +  object Command_Decl {
    2.39 +    def unapply(msg: XML.Tree): Option[(String, String)] =
    2.40 +      msg match {
    2.41 +        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
    2.42 +          Some((name, kind))
    2.43 +        case _ => None
    2.44 +      }
    2.45 +  }
    2.46  }
    2.47