src/Pure/Isar/outer_keyword.scala
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 34166 446a33b874b3
child 36681 dffeca08d3bf
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm@29449
     1
/*  Title:      Pure/Isar/outer_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@34158
    10
object Outer_Keyword
wenzelm@32450
    11
{
wenzelm@29449
    12
  val MINOR = "minor"
wenzelm@29449
    13
  val CONTROL = "control"
wenzelm@29449
    14
  val DIAG = "diag"
wenzelm@29449
    15
  val THY_BEGIN = "theory-begin"
wenzelm@29449
    16
  val THY_SWITCH = "theory-switch"
wenzelm@29449
    17
  val THY_END = "theory-end"
wenzelm@29449
    18
  val THY_HEADING = "theory-heading"
wenzelm@29449
    19
  val THY_DECL = "theory-decl"
wenzelm@29449
    20
  val THY_SCRIPT = "theory-script"
wenzelm@29449
    21
  val THY_GOAL = "theory-goal"
wenzelm@29449
    22
  val QED = "qed"
wenzelm@29449
    23
  val QED_BLOCK = "qed-block"
wenzelm@29449
    24
  val QED_GLOBAL = "qed-global"
wenzelm@29449
    25
  val PRF_HEADING = "proof-heading"
wenzelm@29449
    26
  val PRF_GOAL = "proof-goal"
wenzelm@29449
    27
  val PRF_BLOCK = "proof-block"
wenzelm@29449
    28
  val PRF_OPEN = "proof-open"
wenzelm@29449
    29
  val PRF_CLOSE = "proof-close"
wenzelm@29449
    30
  val PRF_CHAIN = "proof-chain"
wenzelm@29449
    31
  val PRF_DECL = "proof-decl"
wenzelm@29449
    32
  val PRF_ASM = "proof-asm"
wenzelm@29449
    33
  val PRF_ASM_GOAL = "proof-asm-goal"
wenzelm@29449
    34
  val PRF_SCRIPT = "proof-script"
wenzelm@29449
    35
wenzelm@29449
    36
  val minor = Set(MINOR)
wenzelm@29449
    37
  val control = Set(CONTROL)
wenzelm@29449
    38
  val diag = Set(DIAG)
wenzelm@29450
    39
  val heading = Set(THY_HEADING, PRF_HEADING)
wenzelm@29450
    40
  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
wenzelm@29449
    41
  val theory2 = Set(THY_DECL, THY_GOAL)
wenzelm@29450
    42
  val proof1 =
wenzelm@29450
    43
    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
wenzelm@29449
    44
  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
wenzelm@29449
    45
  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
wenzelm@29449
    46
}
wenzelm@29449
    47