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