# HG changeset patch
# User wenzelm
# Date 1717753455 -7200
# Node ID a3a1ec0c47ab35e68ff5a01d39074ea21d32e535
# Parent  00d68f3240567334f406aa459b9a32b608c5060c
clarified signature: separate formal context from exported theory_name;

diff -r 00d68f324056 -r a3a1ec0c47ab src/Pure/Build/export.ML
--- a/src/Pure/Build/export.ML	Fri Jun 07 11:10:49 2024 +0200
+++ b/src/Pure/Build/export.ML	Fri Jun 07 11:44:15 2024 +0200
@@ -6,10 +6,10 @@
 
 signature EXPORT =
 sig
-  val report_export: theory -> Path.binding -> unit
+  val report: Context.generic -> string -> Path.binding -> unit
   type params =
-    {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
-  val export_params: params -> XML.body -> unit
+    {theory_name: string, binding: Path.binding, executable: bool, compress: bool, strict: bool}
+  val export_params: Context.generic -> params -> XML.body -> unit
   val export: theory -> Path.binding -> XML.body -> unit
   val export_executable: theory -> Path.binding -> XML.body -> unit
   val export_file: theory -> Path.binding -> Path.T -> unit
@@ -23,34 +23,35 @@
 
 (* export *)
 
-fun report_export thy binding =
+fun report context theory_name binding =
   let
-    val theory_name = Context.theory_long_name thy;
     val (path, pos) = Path.dest_binding binding;
     val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
-  in Context_Position.report_generic (Context.Theory thy) pos markup end;
+  in Context_Position.report_generic context pos markup end;
 
 type params =
-  {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
+  {theory_name: string, binding: Path.binding, executable: bool, compress: bool, strict: bool};
 
-fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
- (report_export thy binding;
+fun export_params context ({theory_name, binding, executable, compress, strict}: params) body =
+ (report context theory_name binding;
   (Output.try_protocol_message o Markup.export)
    {id = Position.id_of (Position.thread_data ()),
     serial = serial (),
-    theory_name = Context.theory_long_name thy,
+    theory_name = theory_name,
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress,
     strict = strict} [body]);
 
 fun export thy binding body =
-  export_params
-    {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
+  export_params (Context.Theory thy)
+    {theory_name = Context.theory_long_name thy, binding = binding,
+      executable = false, compress = true, strict = true} body;
 
 fun export_executable thy binding body =
-  export_params
-    {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
+  export_params (Context.Theory thy)
+    {theory_name = Context.theory_long_name thy, binding = binding,
+      executable = true, compress = true, strict = true} body;
 
 fun export_file thy binding file =
   export thy binding (Bytes.contents_blob (Bytes.read file));
diff -r 00d68f324056 -r a3a1ec0c47ab src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Jun 07 11:10:49 2024 +0200
+++ b/src/Pure/Tools/generated_files.ML	Fri Jun 07 11:44:15 2024 +0200
@@ -349,7 +349,8 @@
                 (case try Bytes.read (dir + path) of
                   SOME bytes => Bytes.contents_blob bytes
                 | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
-              val _ = Export.report_export thy export_prefix;
+              val _ =
+                Export.report (Context.Theory thy) (Context.theory_long_name thy) export_prefix;
               val binding' =
                 Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
             in
diff -r 00d68f324056 -r a3a1ec0c47ab src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jun 07 11:10:49 2024 +0200
+++ b/src/Pure/proofterm.ML	Fri Jun 07 11:44:15 2024 +0200
@@ -2164,8 +2164,8 @@
         val encode_proof = encode_standard_proof consts;
       in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
   in
-    Export.export_params
-     {theory = thy,
+    Export.export_params (Context.Theory thy)
+     {theory_name = Context.theory_long_name thy,
       binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
       executable = false,
       compress = true,