clarified data representation;

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

--- 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: "