# HG changeset patch
# User wenzelm
# Date 1623007043 -7200
# Node ID 1192c68ebe1c0f8d2603ae4651c947a4972cc9c8
# Parent  9ead8d9be3ab30597535e01eed3f52e66f25c66b
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;

diff -r 9ead8d9be3ab -r 1192c68ebe1c src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Jun 06 20:29:52 2021 +0200
+++ b/src/HOL/ROOT	Sun Jun 06 21:17:23 2021 +0200
@@ -939,7 +939,8 @@
 
 session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL +
   description "Some arbitrary small test case for Mirabelle."
-  options [timeout = 60, mirabelle_actions = "arith"]
+  options [timeout = 60,
+    mirabelle_theories = "HOL-Analysis.Inner_Product", mirabelle_actions = "arith"]
   sessions
     "HOL-Analysis"
   theories
diff -r 9ead8d9be3ab -r 1192c68ebe1c src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Jun 06 20:29:52 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Jun 06 21:17:23 2021 +0200
@@ -147,13 +147,16 @@
     fun check_pos range = check_line range o Position.line_of;
   in check_pos o get_theory end;
 
+fun check_session qualifier thy_name (_: Position.T) =
+  Resources.theory_qualifier thy_name = qualifier;
+
 
 (* presentation hook *)
 
 val whitelist = ["apply", "by", "proof"];
 
 val _ =
-  Build.add_hook (fn loaded_theories =>
+  Build.add_hook (fn qualifier => 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>;
@@ -164,7 +167,9 @@
         (case read_actions mirabelle_actions of
           SOME actions => actions
         | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions));
-      val check = check_theories (space_explode "," mirabelle_theories);
+      val check =
+        if mirabelle_theories = "" then check_session qualifier
+        else check_theories (space_explode "," mirabelle_theories);
 
       fun theory_commands (thy, segments) =
         let
diff -r 9ead8d9be3ab -r 1192c68ebe1c src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun Jun 06 20:29:52 2021 +0200
+++ b/src/Pure/Tools/build.ML	Sun Jun 06 21:17:23 2021 +0200
@@ -6,7 +6,8 @@
 
 signature BUILD =
 sig
-  val add_hook: ((theory * Document_Output.segment list) list -> unit) -> unit
+  type hook = string -> (theory * Document_Output.segment list) list -> unit
+  val add_hook: hook -> unit
 end;
 
 structure Build: BUILD =
@@ -28,17 +29,17 @@
 
 (* build theories *)
 
+type hook = string -> (theory * Document_Output.segment list) list -> unit;
+
 local
-  val hooks =
-    Synchronized.var "Build.hooks"
-      ([]: ((theory * Document_Output.segment list) list -> unit) list);
+  val hooks = Synchronized.var "Build.hooks" ([]: hook list);
 in
 
 fun add_hook hook = Synchronized.change hooks (cons hook);
 
-fun apply_hooks loaded_theories =
+fun apply_hooks qualifier loaded_theories =
   Synchronized.value hooks
-  |> List.app (fn hook => hook loaded_theories);
+  |> List.app (fn hook => hook qualifier loaded_theories);
 
 end;
 
@@ -64,7 +65,7 @@
       else
        (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
           " (undefined " ^ commas conds ^ ")\n"); [])
-  in apply_hooks loaded_theories end;
+  in apply_hooks qualifier loaded_theories end;
 
 
 (* build session *)