clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);

--- a/etc/options	Sun Jun 06 16:34:57 2021 +0200
+++ b/etc/options	Sun Jun 06 20:29:52 2021 +0200
@@ -91,8 +91,6 @@
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
-option parallel_presentation : bool = true
-  -- "parallel theory presentation"
 
 option command_timing_threshold : real = 0.1
   -- "default threshold for persistent command timing (seconds)"

--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Jun 06 16:34:57 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Jun 06 20:29:52 2021 +0200
@@ -153,7 +153,7 @@
 val whitelist = ["apply", "by", "proof"];
 
 val _ =
-  Theory.setup (Thy_Info.add_presentation (fn {segments, ...} => fn thy =>
+  Build.add_hook (fn loaded_theories =>
     let
       val mirabelle_timeout = Options.default_seconds \<^system_option>\<open>mirabelle_timeout\<close>;
       val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>;
@@ -165,26 +165,33 @@
           SOME actions => actions
         | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions));
       val check = check_theories (space_explode "," mirabelle_theories);
-      val commands =
-        segments
-        |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) =>
-          if n mod mirabelle_stride = 0 then
-            let
-              val name = Toplevel.name_of tr;
-              val pos = Toplevel.pos_of tr;
-            in
-              if can (Proof.assert_backward o Toplevel.proof_of) st andalso
-                member (op =) whitelist name andalso
-                check (Context.theory_long_name thy) pos
-              then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'}
-              else NONE
-            end
-          else NONE)
-        |> map_filter I;
 
-      fun apply (i, (name, arguments)) () =
-        apply_action (i + 1) name arguments mirabelle_timeout commands thy;
-    in if null commands then () else fold_index apply actions () end));
+      fun theory_commands (thy, segments) =
+        let
+          val commands = segments
+            |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) =>
+              if n mod mirabelle_stride = 0 then
+                let
+                  val name = Toplevel.name_of tr;
+                  val pos = Toplevel.pos_of tr;
+                in
+                  if can (Proof.assert_backward o Toplevel.proof_of) st andalso
+                    member (op =) whitelist name andalso
+                    check (Context.theory_long_name thy) pos
+                  then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'}
+                  else NONE
+                end
+              else NONE)
+            |> map_filter I;
+        in if null commands then NONE else SOME (thy, commands) end;
+
+      fun app_actions (thy, commands) =
+        (actions, ()) |-> fold_index (fn (index, (name, arguments)) => fn () =>
+          apply_action (index + 1) name arguments mirabelle_timeout commands thy);
+    in
+      if null actions then ()
+      else List.app app_actions (map_filter theory_commands loaded_theories)
+    end);
 
 
 (* Mirabelle utility functions *)

--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun Jun 06 16:34:57 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun Jun 06 20:29:52 2021 +0200
@@ -102,7 +102,7 @@
 
     if (build_results0.ok) {
       val build_options =
-        options + "timeout_build=false" + "parallel_presentation=false" +
+        options + "timeout_build=false" +
           ("mirabelle_actions=" + actions.mkString(";")) +
           ("mirabelle_theories=" + theories.mkString(","))
 

--- a/src/Pure/Thy/thy_info.ML	Sun Jun 06 16:34:57 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 06 20:29:52 2021 +0200
@@ -18,7 +18,8 @@
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
-  val use_theories: Options.T -> string -> (string * Position.T) list -> unit
+  val use_theories: Options.T -> string -> (string * Position.T) list ->
+    (theory * Document_Output.segment list) list
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
@@ -47,14 +48,8 @@
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
-fun sequential_presentation options =
-  not (Options.bool options \<^system_option>\<open>parallel_presentation\<close>);
-
 fun apply_presentation (context: presentation_context) thy =
-  Par_List.map'
-    {name = "apply_presentation", sequential = sequential_presentation (#options context)}
-    (fn (f, _) => f context thy) (Presentation.get thy)
-  |> ignore;
+  ignore (Par_List.map (fn (f, _) => f context thy) (Presentation.get thy));
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
@@ -186,14 +181,20 @@
 (* scheduling loader tasks *)
 
 datatype result =
-  Result of {theory: theory, exec_id: Document_ID.exec,
-    present: (unit -> unit) option, commit: unit -> unit};
+  Result of
+   {theory: theory,
+    exec_id: Document_ID.exec,
+    present: unit -> presentation_context option,
+    commit: unit -> unit};
 
 fun theory_result theory =
-  Result {theory = theory, exec_id = Document_ID.none, present = NONE, commit = I};
+  Result
+   {theory = theory,
+    exec_id = Document_ID.none,
+    present = K NONE,
+    commit = I};
 
 fun result_theory (Result {theory, ...}) = theory;
-fun result_present (Result {present, ...}) = present;
 fun result_commit (Result {commit, ...}) = commit;
 
 fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn]
@@ -204,6 +205,14 @@
         val exns = maps Task_Queue.group_status (Execution.peek exec_id);
       in res :: map Exn.Exn exns end;
 
+fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
+  | present_theory (Exn.Res (Result {theory, present, ...})) =
+      (case present () of
+        NONE => []
+      | SOME (context as {segments, ...}) =>
+          [Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
+
+
 datatype task =
   Task of string list * (theory list -> result) |
   Finished of theory;
@@ -231,18 +240,16 @@
 
     val results1 = futures |> maps (consolidate_theory o Future.join_result);
 
-    val results2 = futures
-      |> map_filter (Option.mapPartial result_present o Exn.get_res o Future.join_result)
-      |> Par_List.map'
-          {name = "present", sequential = sequential_presentation (Options.default ())}
-          (fn present => Exn.capture present ());
+    val present_results = futures |> maps (present_theory o Future.join_result);
+    val results2 = (map o Exn.map_res) (K ()) present_results;
 
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
-  in ignore (Par_Exn.release_all (results1 @ results2 @ results3 @ results4)) end);
+    val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
+  in Par_Exn.release_all present_results end);
 
 
 (* eval theory *)
@@ -284,14 +291,12 @@
 
     val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion;
 
-    fun present () =
+    fun present () : presentation_context =
       let
         val segments =
           (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) =>
             {span = span, prev_state = st, command = tr, state = st'});
-        val context: presentation_context =
-          {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
-      in apply_presentation context thy end;
+      in {options = options, file_pos = text_pos, adjust_pos = I, segments = segments} end;
 
   in (thy, present) end;
 
@@ -339,7 +344,7 @@
     val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
     fun commit () = update_thy deps theory;
-  in Result {theory = theory, exec_id = exec_id, present = SOME present, commit = commit} end;
+  in Result {theory = theory, exec_id = exec_id, present = SOME o present, commit = commit} end;
 
 fun check_thy_deps dir name =
   (case lookup_deps name of
@@ -412,7 +417,7 @@
   schedule_theories (#2 (require_thys options [] qualifier Path.current imports String_Graph.empty));
 
 fun use_thy name =
-  use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)];
+  ignore (use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]);
 
 
 (* toplevel scripting -- without maintaining database *)

--- a/src/Pure/Tools/build.ML	Sun Jun 06 16:34:57 2021 +0200
+++ b/src/Pure/Tools/build.ML	Sun Jun 06 20:29:52 2021 +0200
@@ -4,7 +4,12 @@
 Build Isabelle sessions.
 *)
 
-structure Build: sig end =
+signature BUILD =
+sig
+  val add_hook: ((theory * Document_Output.segment list) list -> unit) -> unit
+end;
+
+structure Build: BUILD =
 struct
 
 (* session timing *)
@@ -23,28 +28,43 @@
 
 (* build theories *)
 
+local
+  val hooks =
+    Synchronized.var "Build.hooks"
+      ([]: ((theory * Document_Output.segment list) list -> unit) list);
+in
+
+fun add_hook hook = Synchronized.change hooks (cons hook);
+
+fun apply_hooks loaded_theories =
+  Synchronized.value hooks
+  |> List.app (fn hook => hook loaded_theories);
+
+end;
+
+
 fun build_theories qualifier (options, thys) =
   let
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
-  in
-    if null conds then
-      (Options.set_default options;
-        Isabelle_Process.init_options ();
-        Future.fork I;
-        (Thy_Info.use_theories options qualifier
-        |>
-          (case Options.string options "profiling" of
-            "" => I
-          | "time" => profile_time
-          | "allocations" => profile_allocations
-          | bad => error ("Bad profiling option: " ^ quote bad))
-        |> Unsynchronized.setmp print_mode
-            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
-    else
-      Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
-        " (undefined " ^ commas conds ^ ")\n")
-  end;
+    val loaded_theories =
+      if null conds then
+        (Options.set_default options;
+          Isabelle_Process.init_options ();
+          Future.fork I;
+          (Thy_Info.use_theories options qualifier
+          |>
+            (case Options.string options "profiling" of
+              "" => I
+            | "time" => profile_time
+            | "allocations" => profile_allocations
+            | bad => error ("Bad profiling option: " ^ quote bad))
+          |> Unsynchronized.setmp print_mode
+              (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
+      else
+       (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
+          " (undefined " ^ commas conds ^ ")\n"); [])
+  in apply_hooks loaded_theories end;
 
 
 (* build session *)