# HG changeset patch
# User wenzelm
# Date 1475601979 -7200
# Node ID fd454d9e97c456e1daa5127baa029bb35432f745
# Parent  84f283385091ca9303562b411486b80eb4666b2d
tuned signature;

diff -r 84f283385091 -r fd454d9e97c4 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Oct 04 18:26:26 2016 +0200
+++ b/src/Pure/Tools/build.scala	Tue Oct 04 19:26:19 2016 +0200
@@ -348,31 +348,30 @@
   }
 
 
-  /* log files */
+  /* session log files */
 
   private val SESSION_NAME = "\fSession.name = "
 
-  sealed case class Log_Info(
-    name: String,
-    stats: List[Properties.T],
-    tasks: List[Properties.T],
+  sealed case class Session_Log_Info(
+    session_name: String,
+    session_timing: Properties.T,
     command_timings: List[Properties.T],
-    session_timing: Properties.T)
+    ml_statistics: List[Properties.T],
+    task_statistics: List[Properties.T])
 
-  def parse_log(full_stats: Boolean, text: String): Log_Info =
+  def parse_session_log(lines: List[String], full: Boolean): Session_Log_Info =
   {
-    val lines = split_lines(text)
     val xml_cache = new XML.Cache()
     def parse_lines(prfx: String): List[Properties.T] =
       Props.parse_lines(prfx, lines).map(xml_cache.props(_))
 
-    val name =
+    val session_name =
       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
-    val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil
-    val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil
+    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
     val command_timings = parse_lines("\fcommand_timing = ")
-    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
-    Log_Info(name, stats, tasks, command_timings, session_timing)
+    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
+    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
+    Session_Log_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
   }
 
 
@@ -519,7 +518,7 @@
       }
 
       try {
-        val info = parse_log(false, text)
+        val info = parse_session_log(split_lines(text), false)
         val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
         (info.command_timings, session_timing)
       }
diff -r 84f283385091 -r fd454d9e97c4 src/Pure/Tools/ci_api.scala
--- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 18:26:26 2016 +0200
+++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 19:26:19 2016 +0200
@@ -45,9 +45,12 @@
     session_logs: List[(String, URL)])
   {
     def read_output(): String = Url.read(output)
-    def read_log(full_stats: Boolean, name: String): Build.Log_Info =
-      Build.parse_log(full_stats,
-        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
+    def read_log(name: String, full: Boolean): Build.Session_Log_Info =
+    {
+      val text =
+        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
+      Build.parse_session_log(split_lines(text), full)
+    }
   }
 
   def build_job_builds(job_name: String): List[Build_Info] =
diff -r 84f283385091 -r fd454d9e97c4 src/Pure/Tools/ml_statistics.scala
--- a/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 18:26:26 2016 +0200
+++ b/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 19:26:19 2016 +0200
@@ -22,11 +22,11 @@
 
   final case class Entry(time: Double, data: Map[String, Double])
 
-  def apply(name: String, stats: List[Properties.T]): ML_Statistics =
-    new ML_Statistics(name, stats)
+  def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
+    new ML_Statistics(session_name, ml_statistics)
 
-  def apply(info: Build.Log_Info): ML_Statistics =
-    apply(info.name, info.stats)
+  def apply(info: Build.Session_Log_Info): ML_Statistics =
+    apply(info.session_name, info.ml_statistics)
 
   val empty = apply("", Nil)
 
@@ -59,26 +59,26 @@
       time_fields, speed_fields)
 }
 
-final class ML_Statistics private(val name: String, val stats: List[Properties.T])
+final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T])
 {
   val Now = new Properties.Double("now")
   def now(props: Properties.T): Double = Now.unapply(props).get
 
-  require(stats.forall(props => Now.unapply(props).isDefined))
+  require(ml_statistics.forall(props => Now.unapply(props).isDefined))
 
-  val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
-  val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
+  val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
+  val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
 
   val fields: Set[String] =
     SortedSet.empty[String] ++
-      (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
+      (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name)
         yield x)
 
   val content: List[ML_Statistics.Entry] =
   {
     var last_edge = Map.empty[String, (Double, Double, Double)]
     val result = new mutable.ListBuffer[ML_Statistics.Entry]
-    for (props <- stats) {
+    for (props <- ml_statistics) {
       val time = now(props) - time_start
       require(time >= 0.0)
 
@@ -135,7 +135,7 @@
       GUI_Thread.later {
         new Frame {
           iconImage = GUI.isabelle_image()
-          title = name
+          title = session_name
           contents = Component.wrap(new ChartPanel(c))
           visible = true
         }
diff -r 84f283385091 -r fd454d9e97c4 src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Tue Oct 04 18:26:26 2016 +0200
+++ b/src/Pure/Tools/task_statistics.scala	Tue Oct 04 19:26:19 2016 +0200
@@ -17,22 +17,23 @@
 
 object Task_Statistics
 {
-  def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
-    new Task_Statistics(name, tasks)
+  def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
+    new Task_Statistics(session_name, task_statistics)
 
-  def apply(info: Build.Log_Info): Task_Statistics =
-    apply(info.name, info.tasks)
+  def apply(info: Build.Session_Log_Info): Task_Statistics =
+    apply(info.session_name, info.task_statistics)
 }
 
-final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
+final class Task_Statistics private(
+  val session_name: String, val task_statistics: List[Properties.T])
 {
   private val Task_Name = new Properties.String("task_name")
   private val Run = new Properties.Int("run")
 
   def chart(bins: Int = 100): JFreeChart =
   {
-    val values = new Array[Double](tasks.length)
-    for ((Run(x), i) <- tasks.iterator.zipWithIndex)
+    val values = new Array[Double](task_statistics.length)
+    for ((Run(x), i) <- task_statistics.iterator.zipWithIndex)
       values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000)
 
     val data = new HistogramDataset
@@ -54,7 +55,7 @@
     GUI_Thread.later {
       new Frame {
         iconImage = GUI.isabelle_image()
-        title = name
+        title = session_name
         contents = Component.wrap(new ChartPanel(chart(bins)))
         visible = true
       }