1.1 --- a/src/Pure/General/sha1.scala	Sun Jul 22 00:00:22 2012 +0200
     1.2 +++ b/src/Pure/General/sha1.scala	Sun Jul 22 12:26:41 2012 +0200
     1.3 @@ -48,6 +48,8 @@
     1.4      make_result(digest)
     1.5    }
     1.6  
     1.7 +  def digest(path: Path): Digest = digest(path.file)
     1.8 +
     1.9    def digest(bytes: Array[Byte]): Digest =
    1.10    {
    1.11      val digest = MessageDigest.getInstance("SHA")

     2.1 --- a/src/Pure/System/build.scala	Sun Jul 22 00:00:22 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Sun Jul 22 12:26:41 2012 +0200
     2.3 @@ -52,6 +52,7 @@
     2.4        options: Options,
     2.5        theories: List[(Options, List[Path])],
     2.6        files: List[Path],
     2.7 +      digest: SHA1.Digest,
     2.8        status: Status = Pending)
     2.9  
    2.10  
    2.11 @@ -203,9 +204,11 @@
    2.12          val theories =
    2.13            entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
    2.14          val files = entry.files.map(Path.explode(_))
    2.15 +        val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    2.16 +
    2.17          val info =
    2.18            Session.Info(dir + path, entry.parent,
    2.19 -            entry.description, options ++ entry.options, theories, files)
    2.20 +            entry.description, options ++ entry.options, theories, files, digest)
    2.21  
    2.22          queue1 + (key, info)
    2.23        }
    2.24 @@ -270,10 +273,15 @@
    2.25  
    2.26    sealed case class Node(
    2.27      loaded_theories: Set[String],
    2.28 -    sources: List[Path])
    2.29 +    sources: List[(Path, SHA1.Digest)])
    2.30  
    2.31 -  def dependencies(queue: Session.Queue): Map[String, Node] =
    2.32 -    (Map.empty[String, Node] /: queue.topological_order)(
    2.33 +  sealed case class Deps(deps: Map[String, Node])
    2.34 +  {
    2.35 +    def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
    2.36 +  }
    2.37 +
    2.38 +  def dependencies(queue: Session.Queue): Deps =
    2.39 +    Deps((Map.empty[String, Node] /: queue.topological_order)(
    2.40        { case (deps, (name, info)) =>
    2.41            val preloaded =
    2.42              info.parent match {
    2.43 @@ -288,7 +296,8 @@
    2.44                  map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
    2.45  
    2.46            val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
    2.47 -          val sources =
    2.48 +
    2.49 +          val all_files =
    2.50              thy_deps.map({ case (n, h) =>
    2.51                val thy = Path.explode(n.node).expand
    2.52                val uses =
    2.53 @@ -299,9 +308,10 @@
    2.54                  }
    2.55                thy :: uses
    2.56              }).flatten ::: info.files.map(file => info.dir + file)
    2.57 +          val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList
    2.58  
    2.59            deps + (name -> Node(loaded_theories, sources))
    2.60 -      })
    2.61 +      }))
    2.62  
    2.63  
    2.64  
    2.65 @@ -367,6 +377,7 @@
    2.66    {
    2.67      val options = (Options.init() /: more_options)(_.define_simple(_))
    2.68      val queue = find_sessions(options, all_sessions, sessions, more_dirs)
    2.69 +    val deps = dependencies(queue)
    2.70  
    2.71  
    2.72      // prepare browser info dir
    2.73 @@ -400,7 +411,10 @@
    2.74  
    2.75            val log = log_dir + Path.basic(name)
    2.76            if (rc == 0) {
    2.77 -            File.write_zip(log.ext("gz"), out)
    2.78 +            val sources =
    2.79 +              (info.digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
    2.80 +                .mkString("sources: ", " ", "\n")
    2.81 +            File.write_zip(log.ext("gz"), sources + out)
    2.82            }
    2.83            else {
    2.84              File.write(log, out)