# HG changeset patch
# User wenzelm
# Date 1606232398 -3600
# Node ID 7af210f1f13bf86ced60c1fd6dd0ae3e71e31ee8
# Parent  45cd55248ffdea5a8eaeac89a291c438ab76576c
clarified signature and database layout;

diff -r 45cd55248ffd -r 7af210f1f13b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Nov 23 16:18:22 2020 +0100
+++ b/src/Pure/ROOT.ML	Tue Nov 24 16:39:58 2020 +0100
@@ -352,3 +352,4 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
+
diff -r 45cd55248ffd -r 7af210f1f13b src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Mon Nov 23 16:18:22 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Tue Nov 24 16:39:58 2020 +0100
@@ -12,9 +12,15 @@
 
 object Presentation
 {
-  /* document variants */
+  /* document info */
 
-  type Document_PDF = (Document_Variant, Bytes)
+  abstract class Document_Name
+  {
+    def name: String
+    def path: Path = Path.basic(name)
+
+    override def toString: String = name
+  }
 
   object Document_Variant
   {
@@ -29,13 +35,11 @@
       }
   }
 
-  sealed case class Document_Variant(name: String, tags: List[String], sources: String = "")
+  sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name
   {
     def print_tags: String = tags.mkString(",")
     def print: String = if (tags.isEmpty) name else name + "=" + print_tags
 
-    def path: Path = Path.basic(name)
-
     def latex_sty: String =
       Library.terminate_lines(
         tags.map(tag =>
@@ -45,8 +49,15 @@
             case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
             case cs => "\\isakeeptag{" + cs.mkString + "}"
           }))
+  }
 
-    def set_sources(s: String): Document_Variant = copy(sources = s)
+  sealed case class Document_Input(name: String, sources: SHA1.Digest)
+    extends Document_Name
+
+  sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
+    extends Document_Name
+  {
+    def log: String = log_xz.uncompress().text
   }
 
 
@@ -56,32 +67,30 @@
   {
     val session_name = SQL.Column.string("session_name").make_primary_key
     val name = SQL.Column.string("name").make_primary_key
-    val tags = SQL.Column.string("tags")
     val sources = SQL.Column.string("sources")
+    val log_xz = SQL.Column.bytes("log_xz")
     val pdf = SQL.Column.bytes("pdf")
 
-    val table = SQL.Table("isabelle_documents", List(session_name, name, tags, sources, pdf))
+    val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
       "WHERE " + Data.session_name.equal(session_name) +
         (if (name == "") "" else " AND " + Data.name.equal(name))
   }
 
-  def read_document_variants(db: SQL.Database, session_name: String): List[Document_Variant] =
+  def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
   {
-    val select =
-      Data.table.select(List(Data.name, Data.tags, Data.sources), Data.where_equal(session_name))
+    val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>
       {
         val name = res.string(Data.name)
-        val tags = res.string(Data.tags)
         val sources = res.string(Data.sources)
-        Document_Variant.parse(name, tags).set_sources(sources)
+        Document_Input(name, SHA1.fake(sources))
       }).toList)
   }
 
-  def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_PDF] =
+  def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
   {
     val select = Data.table.select(sql = Data.where_equal(session_name, name))
     db.using_statement(select)(stmt =>
@@ -89,24 +98,24 @@
       val res = stmt.execute_query()
       if (res.next()) {
         val name = res.string(Data.name)
-        val tags = res.string(Data.tags)
         val sources = res.string(Data.sources)
+        val log_xz = res.bytes(Data.log_xz)
         val pdf = res.bytes(Data.pdf)
-        Some(Document_Variant.parse(name, tags).set_sources(sources) -> pdf)
+        Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf))
       }
       else None
     })
   }
 
-  def write_document(db: SQL.Database, session_name: String, doc: Document_Variant, pdf: Bytes)
+  def write_document(db: SQL.Database, session_name: String, doc: Document_Output)
   {
     db.using_statement(Data.table.insert())(stmt =>
     {
       stmt.string(1) = session_name
       stmt.string(2) = doc.name
-      stmt.string(3) = doc.print_tags
-      stmt.string(4) = doc.sources
-      stmt.bytes(5) = pdf
+      stmt.string(3) = doc.sources.toString
+      stmt.bytes(4) = doc.log_xz
+      stmt.bytes(5) = doc.pdf
       stmt.execute()
     })
   }
@@ -253,8 +262,8 @@
     val documents =
       for {
         doc <- info.document_variants
-        (_, pdf) <- db_context.read_document(session, doc.name)
-      } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc }
+        document <- db_context.read_document(session, doc.name)
+      } yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc }
 
     val links =
     {
@@ -443,7 +452,7 @@
     output_sources: Option[Path] = None,
     output_pdf: Option[Path] = None,
     verbose: Boolean = false,
-    verbose_latex: Boolean = false): List[Document_PDF] =
+    verbose_latex: Boolean = false): List[Document_Output] =
   {
     /* session info */
 
@@ -507,7 +516,7 @@
 
           val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
           val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
-          val sources = SHA1.digest_set(digests).toString
+          val sources = SHA1.digest_set(digests)
           prepare_dir2(tmp_dir, doc)
 
           for (dir <- output_sources) {
@@ -520,12 +529,12 @@
 
           val old_document =
             for {
-              document@(doc, pdf) <- db_context.read_document(session, doc.name)
-              if doc.sources == sources
+              old_doc <- db_context.read_document(session, doc.name)
+              if old_doc.sources == sources
             }
             yield {
-              Bytes.write(doc_dir + doc.path.pdf, pdf)
-              document
+              Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf)
+              old_doc
             }
 
           old_document getOrElse {
@@ -577,16 +586,18 @@
               progress.echo_document("Finished " + session + "/" + doc.name +
                 " (" + timing.message_hms + " elapsed time)")
 
-              doc.set_sources(sources) -> Bytes.read(result_path)
+              val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress()
+              val pdf = Bytes.read(result_path)
+              Document_Output(doc.name, sources, log_xz, pdf)
             }
           }
         })
       }
 
-    for (dir <- output_pdf; (doc, pdf) <- documents) {
+    for (dir <- output_pdf; doc <- documents) {
       Isabelle_System.make_directory(dir)
       val path = dir + doc.path.pdf
-      Bytes.write(path, pdf)
+      Bytes.write(path, doc.pdf)
       progress.echo_document("Document at " + path.absolute)
     }
 
diff -r 45cd55248ffd -r 7af210f1f13b src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Nov 23 16:18:22 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 24 16:39:58 2020 +0100
@@ -1211,7 +1211,7 @@
       read_export(session, theory_name, name) getOrElse
         Export.empty_entry(session, theory_name, name)
 
-    def read_document(session_name: String, name: String): Option[Presentation.Document_PDF] =
+    def read_document(session_name: String, name: String): Option[Presentation.Document_Output] =
       database_server match {
         case Some(db) => Presentation.read_document(db, session_name, name)
         case None =>
diff -r 45cd55248ffd -r 7af210f1f13b src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Nov 23 16:18:22 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Tue Nov 24 16:39:58 2020 +0100
@@ -246,9 +246,9 @@
                   verbose = verbose,
                   verbose_latex = true))
             using(store.open_database(session_name, output = true))(db =>
-              for ((doc, pdf) <- documents) {
+              for (doc <- documents) {
                 db.transaction {
-                  Presentation.write_document(db, session_name, doc, pdf)
+                  Presentation.write_document(db, session_name, doc)
                 }
               })
           }