# HG changeset patch
# User wenzelm
# Date 1637412814 -3600
# Node ID a1fa824315760317a80a371561f49d9bae60b8c7
# Parent  5f73bc0b9e5e42145beb27355fabf720e3e74aa7
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);

diff -r 5f73bc0b9e5e -r a1fa82431576 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Nov 20 12:59:53 2021 +0100
+++ b/src/Pure/Tools/build.ML	Sat Nov 20 13:53:34 2021 +0100
@@ -60,7 +60,7 @@
       else
        (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
           " (undefined " ^ commas conds ^ ")\n"); [])
-  in apply_hooks qualifier loaded_theories end;
+  in loaded_theories end;
 
 
 (* build session *)
@@ -81,11 +81,16 @@
 
           fun build () =
             let
-              val res1 =
+              val res =
                 theories |>
-                  (List.app (build_theories session_name)
+                  (map (build_theories session_name)
                     |> session_timing
                     |> Exn.capture);
+              val res1 =
+                (case res of
+                  Exn.Res loaded_theories =>
+                    Exn.capture (apply_hooks session_name) (flat loaded_theories)
+                | Exn.Exn exn => Exn.Exn exn);
               val res2 = Exn.capture Session.finish ();
 
               val _ = Resources.finish_session_base ();