more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;
--- 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)))
--- 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) =
{