equal
deleted
inserted
replaced
132 |
132 |
133 end; |
133 end; |
134 |
134 |
135 fun check_theories strs = |
135 fun check_theories strs = |
136 let |
136 let |
137 val theories = map read_theory_range strs; |
137 fun theory_import_name s = |
|
138 #theory_name (Resources.import_name (Session.get_name ()) Path.current s); |
|
139 val theories = map read_theory_range strs |
|
140 |> map (apfst theory_import_name); |
138 fun get_theory name = |
141 fun get_theory name = |
139 if null theories then SOME NONE |
142 if null theories then SOME NONE |
140 else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; |
143 else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; |
141 fun check_line NONE _ = false |
144 fun check_line NONE _ = false |
142 | check_line _ NONE = true |
145 | check_line _ NONE = true |
171 val check_theory = check_theories (space_explode "," mirabelle_theories); |
174 val check_theory = check_theories (space_explode "," mirabelle_theories); |
172 |
175 |
173 fun make_commands (thy_index, (thy, segments)) = |
176 fun make_commands (thy_index, (thy, segments)) = |
174 let |
177 let |
175 val thy_long_name = Context.theory_long_name thy; |
178 val thy_long_name = Context.theory_long_name thy; |
176 val thy_name = Context.theory_name thy; |
179 val check_thy = check_theory thy_long_name; |
177 val check_thy = check_theory thy_name; |
|
178 fun make_command {command = tr, prev_state = st, state = st', ...} = |
180 fun make_command {command = tr, prev_state = st, state = st', ...} = |
179 let |
181 let |
180 val name = Toplevel.name_of tr; |
182 val name = Toplevel.name_of tr; |
181 val pos = Toplevel.pos_of tr; |
183 val pos = Toplevel.pos_of tr; |
182 in |
184 in |