src/Pure/System/build.scala

       parent: Option[String],
       description: String,
       options: Options,
       theories: List[(Options, List[Path])],
       files: List[Path],
+      digest: SHA1.Digest,
       status: Status = Pending)
 
 
     /* Queue */
 

         val key = Session.Key(full_name, entry.order)
 
         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)
       }
       catch {
         case ERROR(msg) =>

 
   /* dependencies */
 
   sealed case class Node(
     loaded_theories: Set[String],
-    sources: List[Path])
-
-  def dependencies(queue: Session.Queue): Map[String, Node] =
-    (Map.empty[String, Node] /: queue.topological_order)(
+    sources: List[(Path, SHA1.Digest)])
+
+  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 {
               case None => Set.empty[String]
               case Some(parent) => deps(parent).loaded_theories

             thy_info.dependencies(
               info.theories.map(_._2).flatten.
                 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 =
                 h match {
                   case Exn.Res(d) =>
                     d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
                   case _ => Nil
                 }
               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))
-      })
+      }))
 
 
 
   /** build **/
 

   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
   {
     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
     if (options.bool("browser_info") &&
       !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)

           val (out, err, rc) = build_job(save, name, info).join
           echo_n(err)
 
           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)
             echo(name + " FAILED")
             echo("(see also " + log.file + ")")