src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Mon Oct 02 11:43:17 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 13:33:36 2017 +0200
@@ -815,12 +815,11 @@
       List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
 
     // Build.Session_Info
-    val imported_sources = SQL.Column.string("imported_sources")
     val sources = SQL.Column.string("sources")
     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 build_columns = List(imported_sources, sources, input_heaps, output_heap, return_code)
+    val build_columns = List(sources, input_heaps, output_heap, return_code)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
   }
@@ -909,11 +908,10 @@
           stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
           stmt.bytes(5) = Properties.compress(build_log.task_statistics)
           stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
-          stmt.string(7) = cat_lines(build.imported_sources)
-          stmt.string(8) = cat_lines(build.sources)
-          stmt.string(9) = cat_lines(build.input_heaps)
-          stmt.string(10) = build.output_heap getOrElse ""
-          stmt.int(11) = build.return_code
+          stmt.string(7) = cat_lines(build.sources)
+          stmt.string(8) = cat_lines(build.input_heaps)
+          stmt.string(9) = build.output_heap getOrElse ""
+          stmt.int(10) = build.return_code
           stmt.execute()
         })
       }
@@ -936,34 +934,20 @@
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     {
-      val result0 =
-        db.using_statement(Session_Info.table.select(Session_Info.build_columns.tail,
-          Session_Info.session_name.where_equal(name)))(stmt =>
-        {
-          val res = stmt.execute_query()
-          if (!res.next()) None
-          else {
-            Some(
-              Build.Session_Info(Nil,
-                split_lines(res.string(Session_Info.sources)),
-                split_lines(res.string(Session_Info.input_heaps)),
-                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
-                res.int(Session_Info.return_code)))
-          }
-        })
-      result0.map(info =>
-        info.copy(imported_sources =
-          try {
-            db.using_statement(Session_Info.table.select(List(Session_Info.imported_sources),
-              Session_Info.session_name.where_equal(name)))(stmt =>
-            {
-              val res = stmt.execute_query()
-              if (!res.next) Nil else split_lines(res.string(Session_Info.imported_sources))
-            })
-          } // column "imported_sources" could be missing
-          catch { case _: java.sql.SQLException => Nil }
-        )
-      )
+      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
+        Session_Info.session_name.where_equal(name)))(stmt =>
+      {
+        val res = stmt.execute_query()
+        if (!res.next()) None
+        else {
+          Some(
+            Build.Session_Info(
+              split_lines(res.string(Session_Info.sources)),
+              split_lines(res.string(Session_Info.input_heaps)),
+              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
+              res.int(Session_Info.return_code)))
+        }
+      })
     }
   }
 }