# HG changeset patch
# User wenzelm
# Date 1461143650 -7200
# Node ID 4e7eff53bee77085d83967cc93a0f12737b04b22
# Parent  8b830d2bf94cbf2924c882aaaac58f8a23fe76da
avoid massive multiplication of reports due to interpretation;

diff -r 8b830d2bf94c -r 4e7eff53bee7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Apr 19 15:53:12 2016 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Apr 20 11:14:10 2016 +0200
@@ -449,33 +449,34 @@
 (** Public activation functions **)
 
 fun activate_declarations dep = Context.proof_map (fn context =>
-  let
-    val thy = Context.theory_of context;
-  in
-    roundup thy activate_syntax_decls Morphism.identity dep (Idents.get context, context)
-    |-> Idents.put
-  end);
+  context
+  |> Context_Position.set_visible_generic false
+  |> pair (Idents.get context)
+  |> roundup (Context.theory_of context) activate_syntax_decls Morphism.identity dep
+  |-> Idents.put
+  |> Context_Position.restore_visible_generic context);
 
 fun activate_facts export dep context =
-  let
-    val thy = Context.theory_of context;
-    val activate =
-      activate_notes Element.init'
-        (Morphism.transfer_morphism o Context.theory_of) context export;
-  in
-    roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
-    |-> Idents.put
-  end;
+  context
+  |> Context_Position.set_visible_generic false
+  |> pair (Idents.get context)
+  |> roundup (Context.theory_of context)
+      (activate_notes Element.init' (Morphism.transfer_morphism o Context.theory_of) context export)
+      (the_default Morphism.identity export) dep
+  |-> Idents.put
+  |> Context_Position.restore_visible_generic context;
 
 fun init name thy =
   let
     val context = Context.Proof (Proof_Context.init_global thy);
     val marked = Idents.get context;
-    val (marked', context') = (empty_idents, context)
-      |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of);
   in
-    context'
-    |> Idents.put (merge_idents (marked, marked'))
+    context
+    |> Context_Position.set_visible_generic false
+    |> pair empty_idents
+    |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of)
+    |-> (fn marked' => Idents.put (merge_idents (marked, marked')))
+    |> Context_Position.restore_visible_generic context
     |> Context.proof_of
   end;
 
diff -r 8b830d2bf94c -r 4e7eff53bee7 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Tue Apr 19 15:53:12 2016 +0200
+++ b/src/Pure/context_position.ML	Wed Apr 20 11:14:10 2016 +0200
@@ -14,6 +14,7 @@
   val set_visible_global: bool -> theory -> theory
   val is_really_visible: Proof.context -> bool
   val not_really: Proof.context -> Proof.context
+  val restore_visible_generic: Context.generic -> Context.generic -> Context.generic
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val restore_visible_global: theory -> theory -> theory
   val is_reported_generic: Context.generic -> Position.T -> bool
@@ -49,6 +50,7 @@
 fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt;
 val not_really = Context.proof_map (Data.map (apfst (K (SOME false))));
 
+val restore_visible_generic = Data.put o Data.get;
 val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof;
 val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory;