243 | [] => (Toplevel.ignored range_pos, false) |
243 | [] => (Toplevel.ignored range_pos, false) |
244 | _ => (Toplevel.malformed range_pos not_singleton, true)) |
244 | _ => (Toplevel.malformed range_pos not_singleton, true)) |
245 handle ERROR msg => (Toplevel.malformed range_pos msg, true) |
245 handle ERROR msg => (Toplevel.malformed range_pos msg, true) |
246 end; |
246 end; |
247 |
247 |
|
248 fun prepare_unit parser (cmd, proof) = |
|
249 (case prepare_span parser cmd of |
|
250 (_, false) => NONE |
|
251 | (tr, true) => SOME (tr, map (prepare_span parser) proof |> filter #2 |> map #1)); |
|
252 |
248 fun prepare_command pos str = |
253 fun prepare_command pos str = |
249 let val (lexs, parser) = get_syntax () in |
254 let val (lexs, parser) = get_syntax () in |
250 (case ThyEdit.parse_spans lexs pos str of |
255 (case ThyEdit.parse_spans lexs pos str of |
251 [span] => #1 (prepare_span parser span) |
256 [span] => #1 (prepare_span parser span) |
252 | _ => Toplevel.malformed pos not_singleton) |
257 | _ => Toplevel.malformed pos not_singleton) |
262 val _ = Present.init_theory name; |
267 val _ = Present.init_theory name; |
263 |
268 |
264 val toks = Source.exhausted (ThyEdit.token_source lexs pos (Source.of_list text)); |
269 val toks = Source.exhausted (ThyEdit.token_source lexs pos (Source.of_list text)); |
265 val spans = Source.exhaust (ThyEdit.span_source toks); |
270 val spans = Source.exhaust (ThyEdit.span_source toks); |
266 val _ = List.app ThyEdit.report_span spans; |
271 val _ = List.app ThyEdit.report_span spans; |
267 val trs = map (prepare_span parser) spans |> filter #2 |> map #1; |
272 val units = Source.exhaust (ThyEdit.unit_source (Source.of_list spans)) |
|
273 |> map_filter (prepare_unit parser); |
268 |
274 |
269 val _ = Present.theory_source name |
275 val _ = Present.theory_source name |
270 (fn () => HTML.html_mode (implode o map ThyEdit.present_span) spans); |
276 (fn () => HTML.html_mode (implode o map ThyEdit.present_span) spans); |
271 |
277 |
272 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |
278 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |
273 val _ = cond_timeit time "" (fn () => |
279 val _ = cond_timeit time "" (fn () => |
274 let |
280 let |
275 val (states, commit_exit) = Toplevel.command_excursion trs; |
281 val (results, commit_exit) = Toplevel.excursion units; |
276 val _ = |
282 val _ = |
277 ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (trs ~~ states) toks |
283 ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup results toks |
278 |> Buffer.content |
284 |> Buffer.content |
279 |> Present.theory_output name |
285 |> Present.theory_output name |
280 val _ = commit_exit (); |
286 val _ = commit_exit (); |
281 in () end); |
287 in () end); |
282 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |
288 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |