Tracing of locale activation.

--- a/NEWS	Fri Aug 23 21:08:27 2019 +0200
+++ b/NEWS	Sat Aug 24 12:03:00 2019 +0200
@@ -36,6 +36,9 @@
 terms: it makes a cascade of let-expressions within the derivation tree
 and may thus improve scalability.
 
+* New attribute "trace_locales" for tracing activation of locale
+instances during roundup.
+
 
 *** HOL ***
 

--- a/src/Doc/Isar_Ref/Spec.thy	Fri Aug 23 21:08:27 2019 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Aug 24 12:03:00 2019 +0200
@@ -501,7 +501,7 @@
 subsection \<open>Locale declarations\<close>
 
 text \<open>
-  \begin{matharray}{rcl}
+  \begin{tabular}{rcll}
     @{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
     @{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
     @{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@@ -509,7 +509,8 @@
     @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{method_def intro_locales} & : & \<open>method\<close> \\
     @{method_def unfold_locales} & : & \<open>method\<close> \\
-  \end{matharray}
+    @{attribute_def trace_locales} & : & \<open>attribute\<close> & default \<open>false\<close> \\
+  \end{tabular}
 
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}
@@ -627,6 +628,11 @@
   specifications entailed by the context, both from target statements, and
   from interpretations (see below). New goals that are entailed by the current
   context are discharged automatically.
+
+  \<^descr> @{attribute trace_locales}, when set to
+  \<open>true\<close>, prints the locale instances activated during
+  roundup.  Useful for understanding local theories created by complex
+  locale hierarchies.
 \<close>
 
 

--- a/src/Pure/Isar/locale.ML	Fri Aug 23 21:08:27 2019 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Aug 24 12:03:00 2019 +0200
@@ -433,8 +433,8 @@
 
 (*** Activate context elements of locale ***)
 
-fun activate_err msg (name, morph) context =
-  cat_error msg ("The above error(s) occurred while activating locale instance\n" ^
+fun activate_err msg kind (name, morph) context =
+  cat_error msg ("The above error(s) occurred while activating " ^ kind ^ " of locale instance\n" ^
     (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |>
       Pretty.string_of));
 
@@ -470,14 +470,24 @@
 
 (* Declarations, facts and entire locale content *)
 
+val trace_locales =
+  Attrib.setup_config_bool (Binding.make ("trace_locales", \<^here>)) (K false);
+
+fun trace kind (name, morph) context =
+  if Config.get_generic context trace_locales
+  then tracing ("Activating " ^ kind ^ " of " ^
+    (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of))
+  else ();
+
 fun activate_syntax_decls (name, morph) context =
   let
+    val _ = trace "syntax" (name, morph) context;
     val thy = Context.theory_of context;
     val {syntax_decls, ...} = the_locale thy name;
   in
     context
     |> fold_rev (fn (decl, _) => decl morph) syntax_decls
-      handle ERROR msg => activate_err msg (name, morph) context
+      handle ERROR msg => activate_err msg "syntax" (name, morph) context
   end;
 
 fun activate_notes activ_elem transfer context export' (name, morph) input =
@@ -492,7 +502,14 @@
   in
     (notes', input) |-> fold (fn elem => fn res =>
       activ_elem (Element.transform_ctxt (transfer res) elem) res)
-  end handle ERROR msg => activate_err msg (name, morph) context;
+  end handle ERROR msg => activate_err msg "facts" (name, morph) context;
+
+fun activate_notes_trace activ_elem transfer context export' (name, morph) context' =
+  let
+    val _ = trace "facts" (name, morph) context';
+  in
+    activate_notes activ_elem transfer context export' (name, morph) context'
+  end;
 
 fun activate_all name thy activ_elem transfer (marked, input) =
   let
@@ -517,7 +534,7 @@
   |> Context_Position.set_visible_generic false
   |> pair (Idents.get context)
   |> roundup (Context.theory_of context)
-      (activate_notes init_element Morphism.transfer_morphism'' context export)
+      (activate_notes_trace init_element Morphism.transfer_morphism'' context export)
       (the_default Morphism.identity export) dep
   |-> Idents.put
   |> Context_Position.restore_visible_generic context;