# HG changeset patch
# User wenzelm
# Date 1607356067 -3600
# Node ID 240c8a0f6337f4a08a578a5f767a7acbb38b3b8e
# Parent  dd56ba1974e6ab019cc2def1e223ec5ab407197a
clarified exports;

diff -r dd56ba1974e6 -r 240c8a0f6337 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Dec 07 16:28:44 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Dec 07 16:47:47 2020 +0100
@@ -543,7 +543,7 @@
     val version: Version,
     val node_name: Node.Name,
     edits: List[Text.Edit],
-    snippet_command: Option[Command])
+    val snippet_command: Option[Command])
   {
     override def toString: String =
       "Snapshot(node = " + node_name.node + ", version = " + version.id +
diff -r dd56ba1974e6 -r 240c8a0f6337 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Dec 07 16:28:44 2020 +0100
+++ b/src/Pure/Thy/export.scala	Mon Dec 07 16:47:47 2020 +0100
@@ -15,8 +15,9 @@
 {
   /* artefact names */
 
+  val DOCUMENT_ID = "PIDE/document_id"
+  val FILES = "PIDE/files"
   val MARKUP = "PIDE/markup"
-  val FILES = "PIDE/files"
   val MESSAGES = "PIDE/messages"
   val DOCUMENT_PREFIX = "document/"
   val CITATIONS = DOCUMENT_PREFIX + "citations"
diff -r dd56ba1974e6 -r 240c8a0f6337 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Dec 07 16:28:44 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Dec 07 16:47:47 2020 +0100
@@ -177,17 +177,23 @@
           case snapshot =>
             val rendering = make_rendering(snapshot)
 
-            def export(name: String, xml: XML.Body)
+            def export(name: String, xml: XML.Body, compress: Boolean = true)
             {
               val theory_name = snapshot.node_name.theory
-              val args = Protocol.Export.Args(theory_name = theory_name, name = name)
+              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)
             }
-            def export_text(name: String, text: String): Unit =
-              export(name, List(XML.Text(text)))
+            def export_text(name: String, text: String, compress: Boolean = true): Unit =
+              export(name, List(XML.Text(text)), compress = compress)
 
-            export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.symbolic.node)))
+            for (command <- snapshot.snippet_command) {
+              export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
+            }
+
+            export_text(Export.FILES,
+              cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
 
             for ((xml, i) <- snapshot.xml_markup_blobs().zipWithIndex) {
               export(Export.MARKUP + (i + 1), xml)