diff -r 4e865c45458b -r 11d6a1e62841 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue May 16 17:08:31 2023 +0200 +++ b/src/Pure/Isar/locale.ML Tue May 16 19:20:18 2023 +0200 @@ -107,8 +107,14 @@ type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial}; fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2; +fun transfer_dep thy ({name, morphisms, pos, serial}: dep) : dep = + {name = name, morphisms = apply2 (Morphism.set_context thy) morphisms, pos = pos, serial = serial}; + fun make_dep (name, morphisms) : dep = - {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()}; + {name = name, + morphisms = apply2 Morphism.reset_context morphisms, + pos = Position.thread_data (), + serial = serial ()}; (*table of mixin lists, per list mixins in reverse order of declaration; lists indexed by registration/dependency serial, @@ -120,7 +126,8 @@ val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =); -fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ())); +fun insert_mixin serial' (morph, b) : mixins -> mixins = + Inttab.cons_list (serial', ((Morphism.reset_context morph, b), serial ())); fun rename_mixin (old, new) (mixins: mixins) = (case Inttab.lookup mixins old of @@ -216,8 +223,7 @@ map Element.trim_context_ctxt hyp_spec), ((map (fn decl => (decl, serial ())) syntax_decls, map (fn (a, facts) => ((a, map Attrib.trim_context_fact facts), serial ())) notes), - (map (fn (name, morph) => - make_dep (name, (Morphism.reset_context morph, Morphism.identity))) dependencies, + (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies, Inttab.empty)))) #> snd); (* FIXME Morphism.identity *) @@ -236,15 +242,17 @@ fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy; fun instance_of thy name morph = params_of thy name |> - map (Morphism.term morph o Free o #1); + map (Morphism.term (Morphism.set_context thy morph) o Free o #1); fun specification_of thy = #spec o the_locale thy; -fun hyp_spec_of thy = #hyp_spec o the_locale thy; +fun hyp_spec_of thy = map (Element.transfer_ctxt thy) o #hyp_spec o the_locale thy; + +fun dependencies_of thy = map (transfer_dep thy) o #dependencies o the_locale thy; -fun dependencies_of thy = #dependencies o the_locale thy; - -fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial; +fun mixins_of thy name serial = + lookup_mixins (#mixins (the_locale thy name)) serial + |> (map o apfst o apfst) (Morphism.set_context thy); (* Print instance and qualifiers *) @@ -398,7 +406,10 @@ fun add_reg thy export (name, morph) = let - val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()}; + val reg = + {morphisms = (Morphism.reset_context morph, Morphism.reset_context export), + pos = Position.thread_data (), + serial = serial ()}; val id = (name, instance_of thy name (morph $> export)); in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end; @@ -494,28 +505,28 @@ handle ERROR msg => activate_err msg "syntax" (name, morph) context end; -fun activate_notes activ_elem transfer context export' (name, morph) input = +fun activate_notes activ_elem context export' (name, morph) input = let val thy = Context.theory_of context; val mixin = (case export' of NONE => Morphism.identity | SOME export => collect_mixins context (name, morph $> export) $> export); - val morph' = transfer input $> morph $> mixin; + val morph' = Morphism.set_context thy (morph $> mixin); val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name); in (notes', input) |-> fold (fn elem => fn res => - activ_elem (Element.transform_ctxt (transfer res) elem) res) + activ_elem (Element.transfer_ctxt thy elem) res) end handle ERROR msg => activate_err msg "facts" (name, morph) context; -fun activate_notes_trace activ_elem transfer context export' (name, morph) context' = +fun activate_notes_trace activ_elem context export' (name, morph) context' = let val _ = trace "facts" (name, morph) context'; in - activate_notes activ_elem transfer context export' (name, morph) context' + activate_notes activ_elem context export' (name, morph) context' end; -fun activate_all name thy activ_elem transfer (marked, input) = +fun activate_all name thy activ_elem (marked, input) = let val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name; val input' = input |> @@ -525,7 +536,7 @@ (case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |> (not (null defs) ? activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs))); - val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE; + val activate = activate_notes activ_elem (Context.Theory thy) NONE; in roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input') end; @@ -538,7 +549,7 @@ |> Context_Position.set_visible_generic false |> pair (Idents.get context) |> roundup (Context.theory_of context) - (activate_notes_trace init_element Morphism.transfer_morphism'' context export) + (activate_notes_trace init_element context export) (Morphism.default export) dep |-> Idents.put |> Context_Position.restore_visible_generic context; @@ -559,7 +570,7 @@ context |> Context_Position.set_visible_generic false |> pair empty_idents - |> activate_all name thy init_element Morphism.transfer_morphism'' + |> activate_all name thy init_element |-> (fn marked' => Idents.put (merge_idents (marked, marked'))) |> Context_Position.restore_visible_generic context |> Context.proof_of @@ -735,7 +746,7 @@ | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem | cons_elem elem = cons elem; val elems = - activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, []) + activate_all name thy cons_elem (empty_idents, []) |> snd |> rev |> tap consolidate_notes |> map force_notes;