equal
deleted
inserted
replaced
171 val check_theory = check_theories (space_explode "," mirabelle_theories); |
171 val check_theory = check_theories (space_explode "," mirabelle_theories); |
172 |
172 |
173 fun make_commands (thy_index, (thy, segments)) = |
173 fun make_commands (thy_index, (thy, segments)) = |
174 let |
174 let |
175 val thy_long_name = Context.theory_long_name thy; |
175 val thy_long_name = Context.theory_long_name thy; |
176 val check_thy = check_theory thy_long_name; |
176 val thy_name = Context.theory_name thy; |
|
177 val check_thy = check_theory thy_name; |
177 fun make_command {command = tr, prev_state = st, state = st', ...} = |
178 fun make_command {command = tr, prev_state = st, state = st', ...} = |
178 let |
179 let |
179 val name = Toplevel.name_of tr; |
180 val name = Toplevel.name_of tr; |
180 val pos = Toplevel.pos_of tr; |
181 val pos = Toplevel.pos_of tr; |
181 in |
182 in |