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