# HG changeset patch
# User wenzelm
# Date 1489741380 -3600
# Node ID d189ff34b5b9614cf2088a26854f4a5655df39cd
# Parent  042160aee6c2238f82bb244c14f32b21d993bd3f
clarified data representation;

diff -r 042160aee6c2 -r d189ff34b5b9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 17 09:49:01 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 10:03:00 2017 +0100
@@ -630,8 +630,8 @@
           db.set_bytes(stmt, 3, store.compress_properties(build_log.command_timings))
           db.set_bytes(stmt, 4, store.compress_properties(build_log.ml_statistics))
           db.set_bytes(stmt, 5, store.compress_properties(build_log.task_statistics))
-          db.set_string(stmt, 6, build.sources)
-          db.set_string(stmt, 7, build.input_heaps)
+          db.set_string(stmt, 6, cat_lines(build.sources))
+          db.set_string(stmt, 7, cat_lines(build.input_heaps))
           db.set_string(stmt, 8, build.output_heap)
           db.set_int(stmt, 9, build.return_code)
           stmt.execute()
@@ -656,8 +656,8 @@
               store.uncompress_properties(db.bytes(rs, task_statistics.name)))
           val build =
             Build.Session_Info(
-              db.string(rs, sources.name),
-              db.string(rs, input_heaps.name),
+              split_lines(db.string(rs, sources.name)),
+              split_lines(db.string(rs, input_heaps.name)),
               db.string(rs, output_heap.name),
               db.int(rs, return_code.name))
           Some((build_log, build))
diff -r 042160aee6c2 -r d189ff34b5b9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Mar 17 09:49:01 2017 +0100
+++ b/src/Pure/Tools/build.scala	Fri Mar 17 10:03:00 2017 +0100
@@ -204,7 +204,7 @@
   /* sources and heaps */
 
   sealed case class Session_Info(
-    sources: String, input_heaps: String, output_heap: String, return_code: Int)
+    sources: List[String], input_heaps: List[String], output_heap: String, return_code: Int)
 
   private val SOURCES = "sources: "
   private val INPUT_HEAP = "input_heap: "