# HG changeset patch
# User wenzelm
# Date 1606410324 -3600
# Node ID 01c9b303303611c549ca64e86f8f67f690ab37a5
# Parent  83411077c37be8c1e7bd96709932c0cb06b094e1
more exports from rendering;
suppress empty exports;

diff -r 83411077c37b -r 01c9b3033036 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Nov 26 17:32:43 2020 +0100
+++ b/src/Pure/Thy/export.scala	Thu Nov 26 18:05:24 2020 +0100
@@ -18,6 +18,7 @@
   val MARKUP = "PIDE/markup"
   val MESSAGES = "PIDE/messages"
   val DOCUMENT_PREFIX = "document/"
+  val CITATIONS = DOCUMENT_PREFIX + "citations"
   val THEORY_PREFIX: String = "theory/"
   val PROOFS_PREFIX: String = "proofs/"
 
diff -r 83411077c37b -r 01c9b3033036 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Nov 26 17:32:43 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 26 18:05:24 2020 +0100
@@ -51,6 +51,10 @@
           override val xml_cache: XML.Cache = store.xml_cache
           override val xz_cache: XZ.Cache = store.xz_cache
         }
+      def make_rendering(snapshot: Document.Snapshot): Rendering =
+        new Rendering(snapshot, options, session) {
+          override def model: Document.Model = ???
+        }
 
       object Build_Session_Errors
       {
@@ -160,14 +164,23 @@
       session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
         {
           case snapshot =>
+            val rendering = make_rendering(snapshot)
+
             def export(name: String, xml: XML.Body)
             {
               val theory_name = snapshot.node_name.theory
               val args = Protocol.Export.Args(theory_name = theory_name, name = name)
-              export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
+              val bytes = Bytes(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)))
+
             export(Export.MARKUP, snapshot.xml_markup())
             export(Export.MESSAGES, snapshot.messages.map(_._1))
+
+            val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))
+            export_text(Export.CITATIONS, cat_lines(citations))
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")