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)) } }