# HG changeset patch
# User wenzelm
# Date 1717840068 -7200
# Node ID f3bfec3b02f0b6d7b0e897ba210d34b442af252b
# Parent  f38771b2df1ccbc8a1211ea9edcb52329a155665
clarified signature: more operations;

diff -r f38771b2df1c -r f3bfec3b02f0 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Jun 08 11:32:38 2024 +0200
+++ b/src/Pure/General/name_space.ML	Sat Jun 08 11:47:48 2024 +0200
@@ -28,6 +28,7 @@
   val names_long: bool Config.T
   val names_short: bool Config.T
   val names_unique: bool Config.T
+  val extern_generic: Context.generic -> T -> string -> xstring
   val extern: Proof.context -> T -> string -> xstring
   val extern_ord: Proof.context -> T -> string ord
   val extern_shortest: Proof.context -> T -> string -> xstring
@@ -291,11 +292,11 @@
 val names_short = Config.declare_option_bool ("names_short", \<^here>);
 val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
 
-fun extern ctxt space name =
+fun extern_generic context space name =
   let
-    val names_long = Config.get ctxt names_long;
-    val names_short = Config.get ctxt names_short;
-    val names_unique = Config.get ctxt names_unique;
+    val names_long = Config.get_generic context names_long;
+    val names_short = Config.get_generic context names_short;
+    val names_unique = Config.get_generic context names_unique;
 
     fun extern_chunks require_unique a chunks =
       let val {full_name = c, unique, ...} = intern_chunks space chunks in
@@ -321,6 +322,8 @@
     else extern_names (get_aliases space name)
   end;
 
+val extern = extern_generic o Context.Proof;
+
 fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
 
 fun extern_shortest ctxt =
diff -r f38771b2df1c -r f3bfec3b02f0 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jun 08 11:32:38 2024 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jun 08 11:47:48 2024 +0200
@@ -199,7 +199,8 @@
    (Args.theory -- Scan.lift Parse.embedded_position >>
       (ML_Syntax.print_string o uncurry check)));
 
-fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy);
+fun extern thy =
+  Name_Space.extern_generic (Context.Theory thy) (locale_space thy);
 
 fun markup_extern ctxt =
   Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt));