# HG changeset patch
# User wenzelm
# Date 1674219225 -3600
# Node ID 808412ec2e137f60256ae172a023fa2c2de13fa6
# Parent  34219d664854e67d815c793a8aaba828095171bd
obsolete (see also 01c9b3033036);

diff -r 34219d664854 -r 808412ec2e13 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jan 20 13:42:39 2023 +0100
+++ b/src/Pure/Thy/export.scala	Fri Jan 20 13:53:45 2023 +0100
@@ -20,7 +20,6 @@
   val MESSAGES = "PIDE/messages"
   val DOCUMENT_PREFIX = "document/"
   val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex"
-  val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations"
   val THEORY_PREFIX: String = "theory/"
   val PROOFS_PREFIX: String = "proofs/"
 
diff -r 34219d664854 -r 808412ec2e13 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Jan 20 13:42:39 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Jan 20 13:53:45 2023 +0100
@@ -406,8 +406,6 @@
       session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") {
         case snapshot =>
           if (!progress.stopped) {
-            val rendering = new Rendering(snapshot, options, session)
-
             def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = {
               if (!progress.stopped) {
                 val theory_name = snapshot.node_name.theory
@@ -434,9 +432,6 @@
             }
             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.DOCUMENT_CITATIONS, cat_lines(citations))
           }
       }