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