12 /** keyword classification **/ |
12 /** keyword classification **/ |
13 |
13 |
14 /* kinds */ |
14 /* kinds */ |
15 |
15 |
16 val DIAG = "diag" |
16 val DIAG = "diag" |
17 val HEADING = "heading" |
17 val DOCUMENT_HEADING = "document_heading" |
|
18 val DOCUMENT_BODY = "document_body" |
|
19 val DOCUMENT_RAW = "document_raw" |
18 val THY_BEGIN = "thy_begin" |
20 val THY_BEGIN = "thy_begin" |
19 val THY_END = "thy_end" |
21 val THY_END = "thy_end" |
20 val THY_DECL = "thy_decl" |
22 val THY_DECL = "thy_decl" |
21 val THY_DECL_BLOCK = "thy_decl_block" |
23 val THY_DECL_BLOCK = "thy_decl_block" |
22 val THY_LOAD = "thy_load" |
24 val THY_LOAD = "thy_load" |
37 val PRF_SCRIPT = "prf_script" |
39 val PRF_SCRIPT = "prf_script" |
38 |
40 |
39 |
41 |
40 /* categories */ |
42 /* categories */ |
41 |
43 |
|
44 val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) |
|
45 |
42 val diag = Set(DIAG) |
46 val diag = Set(DIAG) |
43 |
47 |
44 val heading = Set(HEADING) |
48 val document_heading = Set(DOCUMENT_HEADING) |
|
49 val document_body = Set(DOCUMENT_BODY) |
|
50 val document_raw = Set(DOCUMENT_RAW) |
|
51 val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) |
45 |
52 |
46 val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) |
53 val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) |
47 |
54 |
48 val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK) |
55 val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK) |
49 |
56 |
52 val proof = |
59 val proof = |
53 Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, |
60 Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, |
54 PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) |
61 PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) |
55 |
62 |
56 val proof_body = |
63 val proof_body = |
57 Set(DIAG, HEADING, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, |
64 Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, |
58 PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) |
65 PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) |
59 |
66 |
60 val theory_goal = Set(THY_GOAL) |
67 val theory_goal = Set(THY_GOAL) |
61 val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT) |
68 val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT) |
62 val qed = Set(QED, QED_SCRIPT, QED_BLOCK) |
69 val qed = Set(QED, QED_SCRIPT, QED_BLOCK) |
63 val qed_global = Set(QED_GLOBAL) |
70 val qed_global = Set(QED_GLOBAL) |