# HG changeset patch
# User wenzelm
# Date 1606305309 -3600
# Node ID c6981f55e60d1eef2e48c96e2390634e987add9c
# Parent  ed59a506998f6bb76a50eb5667542c9631fa1a1c
tuned signature;

diff -r ed59a506998f -r c6981f55e60d src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 25 12:52:00 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 25 12:55:09 2020 +0100
@@ -59,6 +59,9 @@
   {
     def log: String = log_xz.uncompress().text
     def log_lines: List[String] = split_lines(log)
+
+    def write(db: SQL.Database, session_name: String) =
+      write_document(db, session_name, this)
   }
 
 
diff -r ed59a506998f -r c6981f55e60d src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Nov 25 12:52:00 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Nov 25 12:55:09 2020 +0100
@@ -241,7 +241,7 @@
             using(store.open_database(session_name, output = true))(db =>
               for (doc <- documents) {
                 db.transaction {
-                  Presentation.write_document(db, session_name, doc)
+                  doc.write(db, session_name)
                 }
               })
             (documents.flatMap(_.log_lines), Nil)