store session sources stamp;

--- a/src/Pure/Admin/build_history.scala	Tue Oct 24 18:48:21 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 24 21:20:55 2017 +0200
@@ -253,21 +253,34 @@
           Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
         afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
 
-      build_out_progress.echo("Reading theory timings ...")
-      val theory_timings =
+      build_out_progress.echo("Reading session build info ...")
+      val session_build_info =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
 
-            val properties =
-              if (database.is_file) {
-                using(SQLite.open_database(database))(db =>
-                  try { store.read_theory_timings(db, session_name) }
-                  catch { case ERROR(_) => Nil })
-              }
-              else Nil
+            if (database.is_file) {
+              using(SQLite.open_database(database))(db =>
+              {
+                val theory_timings =
+                  try {
+                    store.read_theory_timings(db, session_name).map(ps =>
+                      Build_Log.Log_File.print_props(Build_Log.THEORY_TIMING_MARKER,
+                        (Build_Log.SESSION_NAME, session_name) :: ps))
+                  }
+                  catch { case ERROR(_) => Nil }
 
-            properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
+                val session_sources =
+                  store.read_build(db, session_name).map(_.sources) match {
+                    case Some(sources) if sources.length == SHA1.digest_length =>
+                      List("Sources " + session_name + " " + sources)
+                    case _ => Nil
+                  }
+
+                theory_timings ::: session_sources
+              })
+            }
+            else Nil
           })
 
       build_out_progress.echo("Reading ML statistics ...")
@@ -328,7 +341,7 @@
       File.write_xz(log_path.ext("xz"),
         terminate_lines(
           Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
-          theory_timings.map(Build_Log.Log_File.print_props(Build_Log.THEORY_TIMING_MARKER, _)) :::
+          session_build_info :::
           ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
           session_errors.map(Build_Log.Log_File.print_props(Build_Log.ERROR_MESSAGE_MARKER, _)) :::
           heap_sizes), XZ.options(6))

--- a/src/Pure/Admin/build_log.scala	Tue Oct 24 18:48:21 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Oct 24 21:20:55 2017 +0200
@@ -464,6 +464,7 @@
     threads: Option[Int] = None,
     timing: Timing = Timing.zero,
     ml_timing: Timing = Timing.zero,
+    sources: Option[String] = None,
     heap_size: Option[Long] = None,
     status: Option[Session_Status.Value] = None,
     errors: List[String] = Nil,
@@ -509,6 +510,7 @@
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
     val Session_Failed = new Regex("""^(\S+) FAILED""")
     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
+    val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
     val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
 
     object Theory_Timing
@@ -532,6 +534,7 @@
     var started = Set.empty[String]
     var failed = Set.empty[String]
     var cancelled = Set.empty[String]
+    var sources = Map.empty[String, String]
     var heap_sizes = Map.empty[String, Long]
     var theory_timings = Map.empty[String, Map[String, Timing]]
     var ml_statistics = Map.empty[String, List[Properties.T]]
@@ -539,8 +542,8 @@
 
     def all_sessions: Set[String] =
       chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
-      failed ++ cancelled ++ started ++ heap_sizes.keySet ++ theory_timings.keySet ++
-      ml_statistics.keySet
+      failed ++ cancelled ++ started ++ sources.keySet ++ heap_sizes.keySet ++
+      theory_timings.keySet ++ ml_statistics.keySet
 
 
     for (line <- log_file.lines) {
@@ -576,6 +579,9 @@
           ml_timing += (name -> Timing(elapsed, cpu, gc))
           threads += (name -> t)
 
+        case Sources(name, s) =>
+          sources += (name -> s)
+
         case Heap(name, Value.Long(size)) =>
           heap_sizes += (name -> size)
 
@@ -621,6 +627,7 @@
               threads = threads.get(name),
               timing = timing.getOrElse(name, Timing.zero),
               ml_timing = ml_timing.getOrElse(name, Timing.zero),
+              sources = sources.get(name),
               heap_size = heap_sizes.get(name),
               status = Some(status),
               errors = errors.getOrElse(name, Nil).reverse,
@@ -701,6 +708,7 @@
     val heap_size = SQL.Column.long("heap_size")
     val status = SQL.Column.string("status")
     val errors = SQL.Column.bytes("errors")
+    val sources = SQL.Column.string("sources")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val known = SQL.Column.bool("known")
 
@@ -711,7 +719,7 @@
       build_log_table("sessions",
         List(log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu,
           timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
-          heap_size, status, errors))
+          heap_size, status, errors, sources))
 
     val theories_table =
       build_log_table("theories",
@@ -995,6 +1003,7 @@
           stmt.long(14) = session.heap_size
           stmt.string(15) = session.status.map(_.toString)
           stmt.bytes(16) = compress_errors(session.errors)
+          stmt.string(17) = session.sources
           stmt.execute()
         }
       })
@@ -1154,6 +1163,7 @@
                 timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc),
                 ml_timing =
                   res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc),
+                sources = res.get_string(Data.sources),
                 heap_size = res.get_long(Data.heap_size),
                 status = res.get_string(Data.status).map(Session_Status.withName(_)),
                 errors = uncompress_errors(res.bytes(Data.errors)),