# HG changeset patch
# User wenzelm
# Date 1659699794 -7200
# Node ID 985c3a64748c2e892bf2a98a60a1996ed1567c9f
# Parent  2a0051496844687dd9d4d25881b3ade579ad5d1e
clarified signature: more uniform treatment of empty exports;

diff -r 2a0051496844 -r 985c3a64748c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 13:34:47 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 13:43:14 2022 +0200
@@ -239,9 +239,9 @@
             (results, true)
           })
 
-    def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
-      if (!progress.stopped) {
-        consumer.send(make_entry(session_name, args, body, cache) -> args.strict)
+    def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
+      if (!progress.stopped && !body.is_empty) {
+        consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
       }
     }
 
diff -r 2a0051496844 -r 985c3a64748c src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Aug 05 13:34:47 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Aug 05 13:43:14 2022 +0200
@@ -315,7 +315,7 @@
           private def export_(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Protocol.Export(args) =>
-                export_consumer(session_name, args, msg.chunk)
+                export_consumer.make_entry(session_name, args, msg.chunk)
                 true
               case _ => false
             }
@@ -353,8 +353,8 @@
                 val theory_name = snapshot.node_name.theory
                 val args =
                   Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress)
-                val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml)))
-                if (!bytes.is_empty) export_consumer(session_name, args, bytes)
+                val body = Bytes(Symbol.encode(YXML.string_of_body(xml)))
+                export_consumer.make_entry(session_name, args, body)
               }
             }
             def export_text(name: String, text: String, compress: Boolean = true): Unit =