# HG changeset patch # User wenzelm # Date 1750680659 -7200 # Node ID 0c83a22d8556834363e7cfa0c360e0a83f5a33ce # Parent a3f9f10da6b05a5fc0d29d224c6bbd3198bad765 more robust: assertion holds, because session.finished_theories provides Snapshot from Document.State.end_theory; diff -r a3f9f10da6b0 -r 0c83a22d8556 src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Mon Jun 23 13:55:09 2025 +0200 +++ b/src/Pure/Build/build_job.scala Mon Jun 23 14:10:59 2025 +0200 @@ -300,6 +300,7 @@ def export_text(name: String, text: String, compress: Boolean = true): Unit = export_(name, List(XML.Text(text)), compress = compress) + assert(snapshot.snippet_commands.length == 1) for (command <- snapshot.snippet_commands) { export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) }