# HG changeset patch
# User wenzelm
# Date 1506951466 -7200
# Node ID 0445cfaf613299c1b4284878808669f05c474217
# Parent  3efac90a11a78ee34dcc9d2d619d0e63e729b05a
more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;

diff -r 3efac90a11a7 -r 0445cfaf6132 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Oct 02 13:45:36 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 15:37:46 2017 +0200
@@ -908,7 +908,7 @@
           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.sources)
+          stmt.string(7) = build.sources
           stmt.string(8) = cat_lines(build.input_heaps)
           stmt.string(9) = build.output_heap getOrElse ""
           stmt.int(10) = build.return_code
@@ -942,7 +942,7 @@
         else {
           Some(
             Build.Session_Info(
-              split_lines(res.string(Session_Info.sources)),
+              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 3efac90a11a7 -r 0445cfaf6132 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 02 13:45:36 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Oct 02 15:37:46 2017 +0200
@@ -24,7 +24,7 @@
   /* persistent build info */
 
   sealed case class Session_Info(
-    sources: List[String],
+    sources: String,
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
@@ -377,9 +377,12 @@
 
     val full_sessions = Sessions.load(build_options, dirs, select_dirs)
 
-    def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
-      (full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name))
-        .map(_.toString).sorted
+    def sources_stamp(deps: Sessions.Deps, name: String): String =
+    {
+      val digests =
+        full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
+      SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
+    }
 
     val (selected, selected_sessions, deps) =
     {