clarified name;
authorwenzelm
Fri Mar 17 09:33:58 2017 +0100 (2017-03-17)
changeset 65282f4c5f10829a0
parent 65281 c70e7d24a16d
child 65283 042160aee6c2
clarified name;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Mar 16 23:33:39 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 09:33:58 2017 +0100
     1.3 @@ -602,13 +602,13 @@
     1.4  
     1.5      // Build.Session_Info
     1.6      val sources = SQL.Column.string("sources")
     1.7 -    val input_heap = SQL.Column.string("input_heap")
     1.8 +    val input_heaps = SQL.Column.string("input_heaps")
     1.9      val output_heap = SQL.Column.string("output_heap")
    1.10      val return_code = SQL.Column.int("return_code")
    1.11  
    1.12      val table = SQL.Table("isabelle_session_info",
    1.13        List(session_name, session_timing, command_timings, ml_statistics, task_statistics,
    1.14 -        sources, input_heap, output_heap, return_code))
    1.15 +        sources, input_heaps, output_heap, return_code))
    1.16  
    1.17      def write_data(db: SQLite.Database, info1: Build_Log.Session_Info, info2: Build.Session_Info)
    1.18      {
    1.19 @@ -623,7 +623,7 @@
    1.20            db.set_bytes(stmt, 4, compress_properties(info1.ml_statistics))
    1.21            db.set_bytes(stmt, 5, compress_properties(info1.task_statistics))
    1.22            db.set_string(stmt, 6, info2.sources)
    1.23 -          db.set_string(stmt, 7, info2.input_heap)
    1.24 +          db.set_string(stmt, 7, info2.input_heaps)
    1.25            db.set_string(stmt, 8, info2.output_heap)
    1.26            db.set_int(stmt, 9, info2.return_code)
    1.27            stmt.execute()
    1.28 @@ -648,7 +648,7 @@
    1.29            val info2 =
    1.30              Build.Session_Info(
    1.31                db.string(rs, sources.name),
    1.32 -              db.string(rs, input_heap.name),
    1.33 +              db.string(rs, input_heaps.name),
    1.34                db.string(rs, output_heap.name),
    1.35                db.int(rs, return_code.name))
    1.36            Some((info1, info2))
     2.1 --- a/src/Pure/Tools/build.scala	Thu Mar 16 23:33:39 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 09:33:58 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_heap: String, output_heap: String, return_code: Int)
     2.8 +    sources: String, input_heaps: String, output_heap: String, return_code: Int)
     2.9  
    2.10    private val SOURCES = "sources: "
    2.11    private val INPUT_HEAP = "input_heap: "