# HG changeset patch
# User wenzelm
# Date 1493455982 -7200
# Node ID ee917f172912efb8f06cc61f6d2b3832e5026a42
# Parent  c41bbf657310f9542e1f740cb290c6fbf47fecbd
clarified database content;

diff -r c41bbf657310 -r ee917f172912 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Apr 29 10:50:48 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Apr 29 10:53:02 2017 +0200
@@ -443,6 +443,8 @@
     status: Session_Status.Value,
     ml_statistics: List[Properties.T])
   {
+    def proper_chapter: Option[String] = if (chapter == "") None else Some(chapter)
+    def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups))
     def finished: Boolean = status == Session_Status.FINISHED
   }
 
@@ -741,8 +743,8 @@
                 for ((session_name, session) <- build_info.sessions.iterator) {
                   db.set_string(stmt, 1, log_file.name)
                   db.set_string(stmt, 2, session_name)
-                  db.set_string(stmt, 3, session.chapter)
-                  db.set_string(stmt, 4, cat_lines(session.groups))
+                  db.set_string(stmt, 3, session.proper_chapter)
+                  db.set_string(stmt, 4, session.proper_groups)
                   db.set_int(stmt, 5, session.threads)
                   db.set_long(stmt, 6, session.timing.elapsed.proper_ms)
                   db.set_long(stmt, 7, session.timing.cpu.proper_ms)
@@ -752,7 +754,7 @@
                   db.set_long(stmt, 11, session.ml_timing.gc.proper_ms)
                   db.set_long(stmt, 12, session.heap_size)
                   db.set_string(stmt, 13, session.status.toString)
-                  db.set_bytes(stmt, 14, compress_properties(session.ml_statistics))
+                  db.set_bytes(stmt, 14, compress_properties(session.ml_statistics).proper)
                   stmt.execute()
                 }
               })