76 |
81 |
77 val control = kind "control"; |
82 val control = kind "control"; |
78 val diag = kind "diag"; |
83 val diag = kind "diag"; |
79 val thy_begin = kind "thy_begin"; |
84 val thy_begin = kind "thy_begin"; |
80 val thy_end = kind "thy_end"; |
85 val thy_end = kind "thy_end"; |
81 val thy_heading = kind "thy_heading"; |
86 val thy_heading1 = kind "thy_heading1"; |
|
87 val thy_heading2 = kind "thy_heading2"; |
|
88 val thy_heading3 = kind "thy_heading3"; |
|
89 val thy_heading4 = kind "thy_heading4"; |
82 val thy_decl = kind "thy_decl"; |
90 val thy_decl = kind "thy_decl"; |
83 val thy_script = kind "thy_script"; |
91 val thy_script = kind "thy_script"; |
84 val thy_goal = kind "thy_goal"; |
92 val thy_goal = kind "thy_goal"; |
85 val thy_schematic_goal = kind "thy_schematic_goal"; |
93 val thy_schematic_goal = kind "thy_schematic_goal"; |
86 val qed = kind "qed"; |
94 val qed = kind "qed"; |
87 val qed_block = kind "qed_block"; |
95 val qed_block = kind "qed_block"; |
88 val qed_global = kind "qed_global"; |
96 val qed_global = kind "qed_global"; |
89 val prf_heading = kind "prf_heading"; |
97 val prf_heading2 = kind "prf_heading2"; |
|
98 val prf_heading3 = kind "prf_heading3"; |
|
99 val prf_heading4 = kind "prf_heading4"; |
90 val prf_goal = kind "prf_goal"; |
100 val prf_goal = kind "prf_goal"; |
91 val prf_block = kind "prf_block"; |
101 val prf_block = kind "prf_block"; |
92 val prf_open = kind "prf_open"; |
102 val prf_open = kind "prf_open"; |
93 val prf_close = kind "prf_close"; |
103 val prf_close = kind "prf_close"; |
94 val prf_chain = kind "prf_chain"; |
104 val prf_chain = kind "prf_chain"; |
96 val prf_asm = kind "prf_asm"; |
106 val prf_asm = kind "prf_asm"; |
97 val prf_asm_goal = kind "prf_asm_goal"; |
107 val prf_asm_goal = kind "prf_asm_goal"; |
98 val prf_script = kind "prf_script"; |
108 val prf_script = kind "prf_script"; |
99 |
109 |
100 val kinds = |
110 val kinds = |
101 [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal, |
111 [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4, |
102 thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, |
112 thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global, |
|
113 prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open, |
103 prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]; |
114 prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]; |
104 |
115 |
105 |
116 |
106 (* tags *) |
117 (* tags *) |
107 |
118 |
220 |
231 |
221 val is_diag = command_category [diag]; |
232 val is_diag = command_category [diag]; |
222 val is_control = command_category [control]; |
233 val is_control = command_category [control]; |
223 val is_regular = not o command_category [diag, control]; |
234 val is_regular = not o command_category [diag, control]; |
224 |
235 |
225 val is_heading = command_category [thy_heading, prf_heading]; |
236 val is_heading = |
|
237 command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4, |
|
238 prf_heading2, prf_heading3, prf_heading4]; |
226 |
239 |
227 val is_theory_begin = command_category [thy_begin]; |
240 val is_theory_begin = command_category [thy_begin]; |
228 |
241 |
229 val is_theory = command_category |
242 val is_theory = command_category |
230 [thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal]; |
243 [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4, |
|
244 thy_decl, thy_script, thy_goal, thy_schematic_goal]; |
231 |
245 |
232 val is_proof = command_category |
246 val is_proof = command_category |
233 [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, |
247 [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4, |
234 prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]; |
248 prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl, |
|
249 prf_asm, prf_asm_goal, prf_script]; |
235 |
250 |
236 val is_theory_goal = command_category [thy_goal, thy_schematic_goal]; |
251 val is_theory_goal = command_category [thy_goal, thy_schematic_goal]; |
237 val is_proof_goal = command_category [prf_goal, prf_asm_goal]; |
252 val is_proof_goal = command_category [prf_goal, prf_asm_goal]; |
238 val is_schematic_goal = command_category [thy_schematic_goal]; |
253 val is_schematic_goal = command_category [thy_schematic_goal]; |
239 val is_qed = command_category [qed, qed_block]; |
254 val is_qed = command_category [qed, qed_block]; |