# HG changeset patch
# User wenzelm
# Date 1506944016 -7200
# Node ID 888a51e77c6e0f5ab5583ef2101f80fbe86a1301
# Parent  e7ac579b883ce27765c5e79fc910045c5aa2fa7a
sources_stamp refers to full sources;
simplified data storage (again);

diff -r e7ac579b883c -r 888a51e77c6e 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)))
+        }
+      })
     }
   }
 }
diff -r e7ac579b883c -r 888a51e77c6e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 02 11:43:17 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Oct 02 13:33:36 2017 +0200
@@ -24,7 +24,6 @@
   /* persistent build info */
 
   sealed case class Session_Info(
-    imported_sources: List[String],
     sources: List[String],
     input_heaps: List[String],
     output_heap: Option[String],
@@ -375,11 +374,9 @@
 
     val full_sessions = Sessions.load(build_options, dirs, select_dirs)
 
-    def imported_sources_stamp(deps: Sessions.Deps, name: String): List[String] =
-      deps.imported_sources(name).map(_.toString).sorted
-
     def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
-      (full_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
+      (full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name))
+        .map(_.toString).sorted
 
     val (selected, selected_sessions, deps) =
     {
@@ -401,7 +398,6 @@
                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
                   case Some(build)
                   if build.return_code == 0 &&
-                    build.imported_sources == imported_sources_stamp(deps0, name) &&
                     build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
                 }
@@ -537,11 +533,7 @@
                       parse_session_info(
                         command_timings = true, ml_statistics = true, task_statistics = true),
                   build =
-                    Session_Info(
-                      imported_sources_stamp(deps, name),
-                      sources_stamp(deps, name),
-                      input_heaps,
-                      heap_stamp,
+                    Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
                       process_result.rc)))
             }