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;
     1 /*  Title:      Pure/Isar/outer_keyword.scala
     2     Author:     Makarius
     3 
     4 Isar command keyword classification and keyword tables.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Outer_Keyword
    11 {
    12   val MINOR = "minor"
    13   val CONTROL = "control"
    14   val DIAG = "diag"
    15   val THY_BEGIN = "theory-begin"
    16   val THY_SWITCH = "theory-switch"
    17   val THY_END = "theory-end"
    18   val THY_HEADING = "theory-heading"
    19   val THY_DECL = "theory-decl"
    20   val THY_SCRIPT = "theory-script"
    21   val THY_GOAL = "theory-goal"
    22   val QED = "qed"
    23   val QED_BLOCK = "qed-block"
    24   val QED_GLOBAL = "qed-global"
    25   val PRF_HEADING = "proof-heading"
    26   val PRF_GOAL = "proof-goal"
    27   val PRF_BLOCK = "proof-block"
    28   val PRF_OPEN = "proof-open"
    29   val PRF_CLOSE = "proof-close"
    30   val PRF_CHAIN = "proof-chain"
    31   val PRF_DECL = "proof-decl"
    32   val PRF_ASM = "proof-asm"
    33   val PRF_ASM_GOAL = "proof-asm-goal"
    34   val PRF_SCRIPT = "proof-script"
    35 
    36   val minor = Set(MINOR)
    37   val control = Set(CONTROL)
    38   val diag = Set(DIAG)
    39   val heading = Set(THY_HEADING, PRF_HEADING)
    40   val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    41   val theory2 = Set(THY_DECL, THY_GOAL)
    42   val proof1 =
    43     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    44   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    45   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    46 }
    47