equal
deleted
inserted
replaced
277 |
277 |
278 val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text)); |
278 val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text)); |
279 val spans = Source.exhaust (Thy_Syntax.span_source toks); |
279 val spans = Source.exhaust (Thy_Syntax.span_source toks); |
280 val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *) |
280 val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *) |
281 val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans)) |
281 val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans)) |
282 |> Par_List.map (prepare_atom commands init) |> flat; |
282 |> Par_List.map_name "Outer_Syntax.prepare_atom" (prepare_atom commands init) |> flat; |
283 |
283 |
284 val _ = Present.theory_source name |
284 val _ = Present.theory_source name |
285 (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); |
285 (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); |
286 |
286 |
287 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |
287 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |