clarified data representation;
authorwenzelm
Fri Mar 17 10:03:00 2017 +0100 (2017-03-17)
changeset 65284d189ff34b5b9
parent 65283 042160aee6c2
child 65285 92bc225c7633
clarified data representation;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Mar 17 09:49:01 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 10:03:00 2017 +0100
     1.3 @@ -630,8 +630,8 @@
     1.4            db.set_bytes(stmt, 3, store.compress_properties(build_log.command_timings))
     1.5            db.set_bytes(stmt, 4, store.compress_properties(build_log.ml_statistics))
     1.6            db.set_bytes(stmt, 5, store.compress_properties(build_log.task_statistics))
     1.7 -          db.set_string(stmt, 6, build.sources)
     1.8 -          db.set_string(stmt, 7, build.input_heaps)
     1.9 +          db.set_string(stmt, 6, cat_lines(build.sources))
    1.10 +          db.set_string(stmt, 7, cat_lines(build.input_heaps))
    1.11            db.set_string(stmt, 8, build.output_heap)
    1.12            db.set_int(stmt, 9, build.return_code)
    1.13            stmt.execute()
    1.14 @@ -656,8 +656,8 @@
    1.15                store.uncompress_properties(db.bytes(rs, task_statistics.name)))
    1.16            val build =
    1.17              Build.Session_Info(
    1.18 -              db.string(rs, sources.name),
    1.19 -              db.string(rs, input_heaps.name),
    1.20 +              split_lines(db.string(rs, sources.name)),
    1.21 +              split_lines(db.string(rs, input_heaps.name)),
    1.22                db.string(rs, output_heap.name),
    1.23                db.int(rs, return_code.name))
    1.24            Some((build_log, build))
     2.1 --- a/src/Pure/Tools/build.scala	Fri Mar 17 09:49:01 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 10:03:00 2017 +0100
     2.3 @@ -204,7 +204,7 @@
     2.4    /* sources and heaps */
     2.5  
     2.6    sealed case class Session_Info(
     2.7 -    sources: String, input_heaps: String, output_heap: String, return_code: Int)
     2.8 +    sources: List[String], input_heaps: List[String], output_heap: String, return_code: Int)
     2.9  
    2.10    private val SOURCES = "sources: "
    2.11    private val INPUT_HEAP = "input_heap: "