257 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |
257 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |
258 val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements); |
258 val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements); |
259 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |
259 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |
260 |
260 |
261 val present = |
261 val present = |
262 singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE, |
262 Future.flat results |> Future.map (fn res0 => |
263 deps = map Future.task_of results, pri = 0, interrupts = true}) |
263 let |
264 (fn () => |
264 val res = filter_out (Toplevel.is_ignored o #1) res0; |
265 let val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax () in |
265 val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax (); |
|
266 in |
266 Thy_Output.present_thy minor Keyword.command_tags |
267 Thy_Output.present_thy minor Keyword.command_tags |
267 (Outer_Syntax.is_markup outer_syntax) |
268 (Outer_Syntax.is_markup outer_syntax) res toks |
268 (filter_out (Toplevel.is_ignored o #1) (maps Future.join results)) toks |
|
269 |> Buffer.content |
269 |> Buffer.content |
270 |> Present.theory_output name |
270 |> Present.theory_output name |
271 end); |
271 end); |
272 |
272 |
273 in (thy, present) end; |
273 in (thy, present) end; |