# HG changeset patch
# User ballarin
# Date 1567012757 -7200
# Node ID 2fb2e7661e161894a28c643da457c02657585c78
# Parent  1afcfb7fdff41a9b0d1def6e6d3e6f761ea1cbdf
Integrate locale activation fallback diagnostics with 'trace_locales'.

diff -r 1afcfb7fdff4 -r 2fb2e7661e16 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Aug 28 08:51:20 2019 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Aug 28 19:19:17 2019 +0200
@@ -396,7 +396,9 @@
         val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
         val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2
           handle ERROR msg => if null eqns then error msg else
-            (writeln (msg ^ "\nFalling back to reading rewrites clause first."); ctxt2);
+            (Locale.tracing ctxt1
+             (msg ^ "\nFalling back to reading rewrites clause before activation.");
+             ctxt2);
 
         val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
         val eqns' = (prep_eqns ctxt' o map snd) eqns;
diff -r 1afcfb7fdff4 -r 2fb2e7661e16 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Aug 28 08:51:20 2019 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 28 19:19:17 2019 +0200
@@ -96,6 +96,7 @@
     {source: string, target: string, prefix: (string * bool) list, morphism: morphism,
       pos: Position.T, serial: serial}
   val dest_dependencies: theory list -> theory -> locale_dependency list
+  val tracing : Proof.context -> string -> unit
 end;
 
 structure Locale: LOCALE =
@@ -473,11 +474,12 @@
 val trace_locales =
   Attrib.setup_config_bool (Binding.make ("trace_locales", \<^here>)) (K false);
 
+fun tracing context msg =
+  if Config.get context trace_locales then Output.tracing msg else ();
+  
 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 ();
+  tracing (Context.proof_of context) ("Activating " ^ kind ^ " of " ^
+    (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of));
 
 fun activate_syntax_decls (name, morph) context =
   let