# HG changeset patch # User wenzelm # Date 1733134116 -3600 # Node ID fb49af893986484bb521a61efa4e1023b9d8646a # Parent ee8b84bd154b288c5f6f2deae86b7e499e1fda1d proper context for extern/check operation: observe local options like names_unique; diff -r ee8b84bd154b -r fb49af893986 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sun Dec 01 22:14:13 2024 +0100 +++ b/src/Pure/Isar/expression.ML Mon Dec 02 11:08:36 2024 +0100 @@ -66,7 +66,7 @@ (** Internalise locale names in expr **) -fun check_expr thy instances = map (apfst (Locale.check thy)) instances; +fun check_expr ctxt instances = map (apfst (Locale.check ctxt)) instances; (** Parameters of expression **) @@ -378,7 +378,7 @@ let val thy = Proof_Context.theory_of ctxt1; - val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); + val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr ctxt1) raw_import); fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let diff -r ee8b84bd154b -r fb49af893986 src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Sun Dec 01 22:14:13 2024 +0100 +++ b/src/Pure/Isar/interpretation.ML Mon Dec 02 11:08:36 2024 +0100 @@ -215,7 +215,7 @@ gen_global_sublocale (K I) cert_interpretation expression; fun global_sublocale_cmd raw_expression = - gen_global_sublocale Locale.check read_interpretation raw_expression; + gen_global_sublocale Locale.check_global read_interpretation raw_expression; end; diff -r ee8b84bd154b -r fb49af893986 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sun Dec 01 22:14:13 2024 +0100 +++ b/src/Pure/Isar/locale.ML Mon Dec 02 11:08:36 2024 +0100 @@ -44,8 +44,9 @@ (string * morphism) list -> theory -> theory val locale_space: theory -> Name_Space.T val intern: theory -> xstring -> string - val check: theory -> xstring * Position.T -> string - val extern: theory -> string -> xstring + val check_global: theory -> xstring * Position.T -> string + val check: Proof.context -> xstring * Position.T -> string + val extern: Proof.context -> string -> xstring val markup_name: Proof.context -> string -> string val pretty_name: Proof.context -> string -> Pretty.T val defined: theory -> string -> bool @@ -192,14 +193,20 @@ val locale_space = Name_Space.space_of_table o Locales.get; val intern = Name_Space.intern o locale_space; -fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); + +fun check_global thy = + #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); + +fun check ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (Locales.get (Proof_Context.theory_of ctxt)); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\locale\ - (Args.theory -- Scan.lift Parse.embedded_position >> + (Args.context -- Scan.lift Parse.embedded_position >> (ML_Syntax.print_string o uncurry check))); -fun extern thy = Name_Space.extern_global thy (locale_space thy); +fun extern ctxt = + Name_Space.extern ctxt (locale_space (Proof_Context.theory_of ctxt)); fun markup_extern ctxt = Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt)); diff -r ee8b84bd154b -r fb49af893986 src/Pure/Isar/target_context.ML --- a/src/Pure/Isar/target_context.ML Sun Dec 01 22:14:13 2024 +0100 +++ b/src/Pure/Isar/target_context.ML Mon Dec 02 11:08:36 2024 +0100 @@ -25,7 +25,7 @@ fun context_begin_named_cmd raw_includes ("-", _) thy = Named_Target.init (prep_includes thy raw_includes) "" thy | context_begin_named_cmd raw_includes name thy = - Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy; + Named_Target.init (prep_includes thy raw_includes) (Locale.check_global thy name) thy; val end_named_cmd = Context.Theory o Local_Theory.exit_global; diff -r ee8b84bd154b -r fb49af893986 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sun Dec 01 22:14:13 2024 +0100 +++ b/src/Pure/Pure.thy Mon Dec 02 11:08:36 2024 +0100 @@ -1210,7 +1210,8 @@ Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; - val name = Locale.check thy raw_name; + val ctxt = Toplevel.context_of state; + val name = Locale.check ctxt raw_name; in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = @@ -1219,9 +1220,9 @@ (Parse.name_position >> (fn raw_name => Toplevel.keep (fn state => let + val thy = Toplevel.theory_of state; val ctxt = Toplevel.context_of state; - val thy = Toplevel.theory_of state; - val name = Locale.check thy raw_name; + val name = Locale.check ctxt raw_name; in Pretty.writeln (Locale.pretty_registrations ctxt name) end))); val _ = @@ -1257,12 +1258,16 @@ val _ = Outer_Syntax.command \<^command_keyword>\locale_deps\ "visualize locale dependencies" - (Scan.succeed - (Toplevel.keep (Toplevel.theory_of #> (fn thy => + (Scan.succeed (Toplevel.keep (fn state => + let + val thy = Toplevel.theory_of state; + val ctxt = Toplevel.context_of state; + in Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => - ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) - |> Graph_Display.display_graph_old)))); + ((name, Graph_Display.content_node (Locale.extern ctxt name) [body]), parents)) + |> Graph_Display.display_graph_old + end))); val _ = Outer_Syntax.command \<^command_keyword>\print_term_bindings\ diff -r ee8b84bd154b -r fb49af893986 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Sun Dec 01 22:14:13 2024 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Mon Dec 02 11:08:36 2024 +0100 @@ -47,8 +47,7 @@ in Proof_Context.pretty_term_abbrev ctxt' eq end; fun pretty_locale ctxt (name, pos) = - let val thy = Proof_Context.theory_of ctxt - in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end; + Pretty.str (Locale.extern ctxt (Locale.check ctxt (name, pos))); fun pretty_bundle ctxt (name, pos) = Pretty.str (Bundle.extern ctxt (Bundle.check ctxt (name, pos)));