src/Pure/Thy/thy_load.ML

   val load_current: theory -> bool
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
-    Position.T -> string -> theory list -> theory * unit future
+    Position.T -> string -> theory list -> theory * (unit -> unit) * int
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
 end;
 
 structure Thy_Load: THY_LOAD =

 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
     val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
-    val present =
-      Future.flat results |> Future.map (fn res0 =>
-        let
-          val res = filter_out (Toplevel.is_ignored o #1) res0;
-          val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
-        in
-          Thy_Output.present_thy minor Keyword.command_tags
-            (Outer_Syntax.is_markup outer_syntax) res toks
-          |> Buffer.content
-          |> Present.theory_output name
-        end);
-
-  in (thy, present) end;
+    fun present () =
+      let
+        val res = filter_out (Toplevel.is_ignored o #1) (flat (Future.joins results));
+        val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
+      in
+        Thy_Output.present_thy minor Keyword.command_tags
+          (Outer_Syntax.is_markup outer_syntax) res toks
+        |> Buffer.content
+        |> Present.theory_output name
+      end;
+
+  in (thy, present, size text) end;
 
 
 (* document antiquotation *)
 
 val _ =