Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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, 08 Mar 2014 21:31:12 +0100
changeset 55998 f5f9fad3321c
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 file | annotate | diff | comparison | revisions 
--- 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')) =
isabelle