src/Pure/Isar/keyword.scala
author wenzelm
Fri Apr 08 16:34:14 2011 +0200 (2011-04-08)
changeset 42290 b1f544c84040
parent 40459 913e545d9a9b
child 45666 d83797ef0d2d
permissions -rw-r--r--
discontinued special treatment of structure Lexicon;
     1 /*  Title:      Pure/Isar/keyword.scala
     2     Author:     Makarius
     3 
     4 Isar command keyword classification and keyword tables.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Keyword
    11 {
    12   /* kinds */
    13 
    14   val MINOR = "minor"
    15   val CONTROL = "control"
    16   val DIAG = "diag"
    17   val THY_BEGIN = "theory-begin"
    18   val THY_SWITCH = "theory-switch"
    19   val THY_END = "theory-end"
    20   val THY_HEADING = "theory-heading"
    21   val THY_DECL = "theory-decl"
    22   val THY_SCRIPT = "theory-script"
    23   val THY_GOAL = "theory-goal"
    24   val THY_SCHEMATIC_GOAL = "theory-schematic-goal"
    25   val QED = "qed"
    26   val QED_BLOCK = "qed-block"
    27   val QED_GLOBAL = "qed-global"
    28   val PRF_HEADING = "proof-heading"
    29   val PRF_GOAL = "proof-goal"
    30   val PRF_BLOCK = "proof-block"
    31   val PRF_OPEN = "proof-open"
    32   val PRF_CLOSE = "proof-close"
    33   val PRF_CHAIN = "proof-chain"
    34   val PRF_DECL = "proof-decl"
    35   val PRF_ASM = "proof-asm"
    36   val PRF_ASM_GOAL = "proof-asm-goal"
    37   val PRF_SCRIPT = "proof-script"
    38 
    39 
    40   /* categories */
    41 
    42   val minor = Set(MINOR)
    43   val control = Set(CONTROL)
    44   val diag = Set(DIAG)
    45   val theory =
    46     Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT,
    47       THY_GOAL, THY_SCHEMATIC_GOAL)
    48   val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    49   val theory2 = Set(THY_DECL, THY_GOAL)
    50   val proof =
    51     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,
    52       PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
    53   val proof1 =
    54     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    55   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    56   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    57 
    58 
    59   /* protocol messages */
    60 
    61   object Keyword_Decl {
    62     def unapply(msg: XML.Tree): Option[String] =
    63       msg match {
    64         case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name)
    65         case _ => None
    66       }
    67   }
    68 
    69   object Command_Decl {
    70     def unapply(msg: XML.Tree): Option[(String, String)] =
    71       msg match {
    72         case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) =>
    73           Some((name, kind))
    74         case _ => None
    75       }
    76   }
    77 }
    78