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;
authorwenzelm
Sat Mar 08 21:31:12 2014 +0100 (2014-03-08)
changeset 55998f5f9fad3321c
parent 55997 9dc5ce83202c
child 55999 6477fc70cfa0
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;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 08 21:08:10 2014 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 08 21:31:12 2014 +0100
     1.3 @@ -302,7 +302,7 @@
     1.4  in
     1.5  
     1.6  fun partial_evaluation ctxt facts =
     1.7 -  (facts, Context.Proof (Context_Position.set_visible false ctxt)) |->
     1.8 +  (facts, Context.Proof ctxt) |->
     1.9      fold_map (fn ((b, more_atts), fact) => fn context =>
    1.10        let
    1.11          val (fact', (decls, context')) =