tuned signature;
authorwenzelm
Wed, 25 Nov 2020 12:55:09 +0100
changeset 72700 c6981f55e60d
parent 72699 ed59a506998f
child 72701 1c42ac589fa0
tuned signature;
src/Pure/Thy/presentation.scala
src/Pure/Tools/build_job.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)
   }
 
 
--- 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)