# HG changeset patch
# User wenzelm
# Date 1394310672 -3600
# Node ID f5f9fad3321c71b8d778bf1e057d34bece2d14d8
# Parent  9dc5ce83202cde2e2a1807e43bb0253117016207
keep current context visibility for PIDE markup and completion (in contrast to 8e3e004f1c31): Attrib.check_src of 9dc5ce83202c should intern/report attributes once, which happens for local_theory in the (visible) auxiliary context;

diff -r 9dc5ce83202c -r f5f9fad3321c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Mar 08 21:08:10 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Mar 08 21:31:12 2014 +0100
@@ -302,7 +302,7 @@
 in
 
 fun partial_evaluation ctxt facts =
-  (facts, Context.Proof (Context_Position.set_visible false ctxt)) |->
+  (facts, Context.Proof ctxt) |->
     fold_map (fn ((b, more_atts), fact) => fn context =>
       let
         val (fact', (decls, context')) =