proper context for extern/check operation: observe local options like names_unique;

--- 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

--- 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;
 

--- 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>\<open>locale\<close>
-   (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));

--- 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;
 

--- 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>\<open>locale_deps\<close> "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>\<open>print_term_bindings\<close>

--- 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)));