# HG changeset patch
# User wenzelm
# Date 1342952801 -7200
# Node ID 0ccf143a2a6983b514a7757b5bb6688478b0917e
# Parent  9613780a805bcc28ade8f8dea0258a0409cb1591
maintain set of source digests, including relevant parts of session entry;

diff -r 9613780a805b -r 0ccf143a2a69 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Sun Jul 22 00:00:22 2012 +0200
+++ b/src/Pure/General/sha1.scala	Sun Jul 22 12:26:41 2012 +0200
@@ -48,6 +48,8 @@
     make_result(digest)
   }
 
+  def digest(path: Path): Digest = digest(path.file)
+
   def digest(bytes: Array[Byte]): Digest =
   {
     val digest = MessageDigest.getInstance("SHA")
diff -r 9613780a805b -r 0ccf143a2a69 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Sun Jul 22 00:00:22 2012 +0200
+++ b/src/Pure/System/build.scala	Sun Jul 22 12:26:41 2012 +0200
@@ -52,6 +52,7 @@
       options: Options,
       theories: List[(Options, List[Path])],
       files: List[Path],
+      digest: SHA1.Digest,
       status: Status = Pending)
 
 
@@ -203,9 +204,11 @@
         val theories =
           entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
         val files = entry.files.map(Path.explode(_))
+        val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
+
         val info =
           Session.Info(dir + path, entry.parent,
-            entry.description, options ++ entry.options, theories, files)
+            entry.description, options ++ entry.options, theories, files, digest)
 
         queue1 + (key, info)
       }
@@ -270,10 +273,15 @@
 
   sealed case class Node(
     loaded_theories: Set[String],
-    sources: List[Path])
+    sources: List[(Path, SHA1.Digest)])
 
-  def dependencies(queue: Session.Queue): Map[String, Node] =
-    (Map.empty[String, Node] /: queue.topological_order)(
+  sealed case class Deps(deps: Map[String, Node])
+  {
+    def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
+  }
+
+  def dependencies(queue: Session.Queue): Deps =
+    Deps((Map.empty[String, Node] /: queue.topological_order)(
       { case (deps, (name, info)) =>
           val preloaded =
             info.parent match {
@@ -288,7 +296,8 @@
                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
-          val sources =
+
+          val all_files =
             thy_deps.map({ case (n, h) =>
               val thy = Path.explode(n.node).expand
               val uses =
@@ -299,9 +308,10 @@
                 }
               thy :: uses
             }).flatten ::: info.files.map(file => info.dir + file)
+          val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList
 
           deps + (name -> Node(loaded_theories, sources))
-      })
+      }))
 
 
 
@@ -367,6 +377,7 @@
   {
     val options = (Options.init() /: more_options)(_.define_simple(_))
     val queue = find_sessions(options, all_sessions, sessions, more_dirs)
+    val deps = dependencies(queue)
 
 
     // prepare browser info dir
@@ -400,7 +411,10 @@
 
           val log = log_dir + Path.basic(name)
           if (rc == 0) {
-            File.write_zip(log.ext("gz"), out)
+            val sources =
+              (info.digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
+                .mkString("sources: ", " ", "\n")
+            File.write_zip(log.ext("gz"), sources + out)
           }
           else {
             File.write(log, out)