diff -r 2da5562114c5 -r 97b5547f2b17 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -99,7 +99,7 @@
     }
   }
 
-  def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = {
+  def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
     db.execute_statement(Data.table.insert(), body =
       { stmt =>
         stmt.string(1) = session_name
@@ -108,7 +108,6 @@
         stmt.bytes(4) = doc.log_xz
         stmt.bytes(5) = doc.pdf
       })
-  }
 
 
   /* background context */