src/Pure/Isar/keyword.scala
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 36947 285b39022372
child 38230 ed147003de4b
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
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@29449
    24
  val QED = "qed"
wenzelm@29449
    25
  val QED_BLOCK = "qed-block"
wenzelm@29449
    26
  val QED_GLOBAL = "qed-global"
wenzelm@29449
    27
  val PRF_HEADING = "proof-heading"
wenzelm@29449
    28
  val PRF_GOAL = "proof-goal"
wenzelm@29449
    29
  val PRF_BLOCK = "proof-block"
wenzelm@29449
    30
  val PRF_OPEN = "proof-open"
wenzelm@29449
    31
  val PRF_CLOSE = "proof-close"
wenzelm@29449
    32
  val PRF_CHAIN = "proof-chain"
wenzelm@29449
    33
  val PRF_DECL = "proof-decl"
wenzelm@29449
    34
  val PRF_ASM = "proof-asm"
wenzelm@29449
    35
  val PRF_ASM_GOAL = "proof-asm-goal"
wenzelm@29449
    36
  val PRF_SCRIPT = "proof-script"
wenzelm@29449
    37
wenzelm@36681
    38
wenzelm@36681
    39
  /* categories */
wenzelm@36681
    40
wenzelm@29449
    41
  val minor = Set(MINOR)
wenzelm@29449
    42
  val control = Set(CONTROL)
wenzelm@29449
    43
  val diag = Set(DIAG)
wenzelm@29450
    44
  val heading = Set(THY_HEADING, PRF_HEADING)
wenzelm@29450
    45
  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
wenzelm@29449
    46
  val theory2 = Set(THY_DECL, THY_GOAL)
wenzelm@29450
    47
  val proof1 =
wenzelm@29450
    48
    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
wenzelm@29449
    49
  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
wenzelm@29449
    50
  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
wenzelm@36681
    51
wenzelm@36681
    52
wenzelm@36681
    53
  /* reports */
wenzelm@36681
    54
wenzelm@36681
    55
  object Keyword_Decl {
wenzelm@36681
    56
    def unapply(msg: XML.Tree): Option[String] =
wenzelm@36681
    57
      msg match {
wenzelm@36681
    58
        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
wenzelm@36681
    59
        case _ => None
wenzelm@36681
    60
      }
wenzelm@36681
    61
  }
wenzelm@36681
    62
wenzelm@36681
    63
  object Command_Decl {
wenzelm@36681
    64
    def unapply(msg: XML.Tree): Option[(String, String)] =
wenzelm@36681
    65
      msg match {
wenzelm@36681
    66
        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
wenzelm@36681
    67
          Some((name, kind))
wenzelm@36681
    68
        case _ => None
wenzelm@36681
    69
      }
wenzelm@36681
    70
  }
wenzelm@29449
    71
}
wenzelm@29449
    72