1.1 --- a/src/Pure/Isar/keyword.scala	Wed Nov 10 15:17:25 2010 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Wed Nov 10 15:41:29 2010 +0100
     1.3 @@ -21,6 +21,7 @@
     1.4    val THY_DECL = "theory-decl"
     1.5    val THY_SCRIPT = "theory-script"
     1.6    val THY_GOAL = "theory-goal"
     1.7 +  val THY_SCHEMATIC_GOAL = "theory-schematic-goal"
     1.8    val QED = "qed"
     1.9    val QED_BLOCK = "qed-block"
    1.10    val QED_GLOBAL = "qed-global"
    1.11 @@ -42,8 +43,14 @@
    1.12    val control = Set(CONTROL)
    1.13    val diag = Set(DIAG)
    1.14    val heading = Set(THY_HEADING, PRF_HEADING)
    1.15 +  val theory =
    1.16 +    Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT,
    1.17 +      THY_GOAL, THY_SCHEMATIC_GOAL)
    1.18    val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    1.19    val theory2 = Set(THY_DECL, THY_GOAL)
    1.20 +  val proof =
    1.21 +    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,
    1.22 +      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
    1.23    val proof1 =
    1.24      Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    1.25    val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)