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