# HG changeset patch
# User wenzelm
# Date 1489739638 -3600
# Node ID f4c5f10829a064bf65c11320a97c92c80cce0c45
# Parent  c70e7d24a16d23366d7e6c392f1dad9671b9f0f6
clarified name;

diff -r c70e7d24a16d -r f4c5f10829a0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 16 23:33:39 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 09:33:58 2017 +0100
@@ -602,13 +602,13 @@
 
     // Build.Session_Info
     val sources = SQL.Column.string("sources")
-    val input_heap = SQL.Column.string("input_heap")
+    val input_heaps = SQL.Column.string("input_heaps")
     val output_heap = SQL.Column.string("output_heap")
     val return_code = SQL.Column.int("return_code")
 
     val table = SQL.Table("isabelle_session_info",
       List(session_name, session_timing, command_timings, ml_statistics, task_statistics,
-        sources, input_heap, output_heap, return_code))
+        sources, input_heaps, output_heap, return_code))
 
     def write_data(db: SQLite.Database, info1: Build_Log.Session_Info, info2: Build.Session_Info)
     {
@@ -623,7 +623,7 @@
           db.set_bytes(stmt, 4, compress_properties(info1.ml_statistics))
           db.set_bytes(stmt, 5, compress_properties(info1.task_statistics))
           db.set_string(stmt, 6, info2.sources)
-          db.set_string(stmt, 7, info2.input_heap)
+          db.set_string(stmt, 7, info2.input_heaps)
           db.set_string(stmt, 8, info2.output_heap)
           db.set_int(stmt, 9, info2.return_code)
           stmt.execute()
@@ -648,7 +648,7 @@
           val info2 =
             Build.Session_Info(
               db.string(rs, sources.name),
-              db.string(rs, input_heap.name),
+              db.string(rs, input_heaps.name),
               db.string(rs, output_heap.name),
               db.int(rs, return_code.name))
           Some((info1, info2))
diff -r c70e7d24a16d -r f4c5f10829a0 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Mar 16 23:33:39 2017 +0100
+++ b/src/Pure/Tools/build.scala	Fri Mar 17 09:33:58 2017 +0100
@@ -204,7 +204,7 @@
   /* sources and heaps */
 
   sealed case class Session_Info(
-    sources: String, input_heap: String, output_heap: String, return_code: Int)
+    sources: String, input_heaps: String, output_heap: String, return_code: Int)
 
   private val SOURCES = "sources: "
   private val INPUT_HEAP = "input_heap: "