record heap sizes;

--- a/src/Pure/Tools/build_history.scala	Sun Oct 09 15:28:18 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Sun Oct 09 16:24:54 2016 +0200
@@ -263,6 +263,8 @@
         other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) +
           Path.explode(log_name(build_history_date, ml_platform, "M" + threads))
 
+      val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
+
       val meta_info =
         List(Build_Log.Field.build_engine -> BUILD_HISTORY,
           Build_Log.Field.build_host -> build_host,
@@ -271,22 +273,31 @@
           Build_Log.Field.isabelle_version -> isabelle_version)
 
       val ml_statistics =
-        Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info().
-          finished_sessions.flatMap(session_name =>
-            {
-              val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
-              if (session_log.is_file) {
-                Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
-                  ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
-              }
-              else Nil
-            })
+        build_info.finished_sessions.flatMap(session_name =>
+          {
+            val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
+            if (session_log.is_file) {
+              Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
+                ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
+            }
+            else Nil
+          })
+
+      val heap_sizes =
+        build_info.finished_sessions.flatMap(session_name =>
+          {
+            val heap = isabelle_output + Path.explode(session_name)
+            if (heap.is_file)
+              Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
+            else None
+          })
 
       Isabelle_System.mkdirs(log_path.dir)
       File.write_gzip(log_path,
-        cat_lines(
+        Library.terminate_lines(
           Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
-          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))))
+          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
+          heap_sizes))
 
       Output.writeln(log_path.implode, stdout = true)
 

--- a/src/Pure/Tools/build_log.scala	Sun Oct 09 15:28:18 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sun Oct 09 16:24:54 2016 +0200
@@ -357,6 +357,7 @@
     timing: Timing,
     ml_timing: Timing,
     ml_statistics: List[Properties.T],
+    heap_size: Option[Long],
     status: Session_Status.Value)
   {
     def finished: Boolean = status == Session_Status.FINISHED
@@ -401,6 +402,7 @@
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
     val Session_Failed = new Regex("""^(\S+) FAILED""")
     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
+    val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
 
     var chapter = Map.empty[String, String]
     var groups = Map.empty[String, List[String]]
@@ -411,10 +413,11 @@
     var failed = Set.empty[String]
     var cancelled = Set.empty[String]
     var ml_statistics = Map.empty[String, List[Properties.T]]
+    var heap_sizes = Map.empty[String, Long]
 
     def all_sessions: Set[String] =
-      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++
-      ml_timing.keySet ++ failed ++ cancelled ++ started ++ ml_statistics.keySet
+      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
+      failed ++ cancelled ++ started ++ ml_statistics.keySet ++ heap_sizes.keySet
 
 
     for (line <- log_file.lines) {
@@ -450,13 +453,16 @@
           ml_timing += (name -> Timing(elapsed, cpu, gc))
           threads += (name -> t)
 
+        case Heap(name, Value.Long(size)) =>
+          heap_sizes += (name -> size)
+
         case _ if line.startsWith(ML_STATISTICS_MARKER) =>
           val (name, props) =
             Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
               case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
               case _ => log_file.err("malformed ML_statistics " + quote(line))
             }
-          ml_statistics = ml_statistics + (name -> (props :: ml_statistics.getOrElse(name, Nil)))
+          ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
 
         case _ =>
       }
@@ -480,6 +486,7 @@
               timing.getOrElse(name, Timing.zero),
               ml_timing.getOrElse(name, Timing.zero),
               ml_statistics.getOrElse(name, Nil).reverse,
+              heap_sizes.get(name),
               status)
           (name -> entry)
         }):_*)