# HG changeset patch
# User wenzelm
# Date 1475608295 -7200
# Node ID c6160d0b0337948d15ad5dab5d890db7a0535995
# Parent  deb4a786e6f9bfe79977d68c731af29e482d9bad
clarified modules;

diff -r deb4a786e6f9 -r c6160d0b0337 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Oct 04 20:20:21 2016 +0200
+++ b/src/Pure/Tools/build.scala	Tue Oct 04 21:11:35 2016 +0200
@@ -334,53 +334,6 @@
   }
 
 
-  /* inlined properties (YXML) */
-
-  object Props
-  {
-    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
-
-    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
-      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
-
-    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
-      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
-  }
-
-
-  /* session log files */
-
-  private val SESSION_NAME = "\fSession.name = "
-
-  sealed case class Session_Log_Info(
-    session_name: String,
-    session_timing: Properties.T,
-    command_timings: List[Properties.T],
-    ml_statistics: List[Properties.T],
-    task_statistics: List[Properties.T])
-
-  def parse_session_log(name0: String, lines: List[String], full: Boolean): Session_Log_Info =
-  {
-    val xml_cache = new XML.Cache()
-    def parse_lines(prfx: String): List[Properties.T] =
-      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
-
-    val session_name =
-      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
-        case None => name0
-        case Some(name) if name0 == "" || name0 == name => name
-        case Some(name) =>
-          error("Session log for " + quote(name0) + " is actually from " + quote(name))
-      }
-    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
-    val command_timings = parse_lines("\fcommand_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)
-  }
-
-
   /* sources and heaps */
 
   private val SOURCES = "sources: "
@@ -524,7 +477,7 @@
       }
 
       try {
-        val info = parse_session_log(name, split_lines(text), false)
+        val info = Build_Log.parse_session_info(name, split_lines(text), false)
         val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
         (info.command_timings, session_timing)
       }
diff -r deb4a786e6f9 -r c6160d0b0337 src/Pure/Tools/build_log.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build_log.scala	Tue Oct 04 21:11:35 2016 +0200
@@ -0,0 +1,57 @@
+/*  Title:      Pure/Tools/build_log.scala
+    Author:     Makarius
+
+Build log parsing for historic versions, back to "build_history_base".
+*/
+
+package isabelle
+
+
+object Build_Log
+{
+  /* inlined properties (YXML) */
+
+  object Props
+  {
+    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
+
+    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
+      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
+
+    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
+      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
+  }
+
+
+  /* session log: produced by "isabelle build" */
+
+  sealed case class Session_Info(
+    session_name: String,
+    session_timing: Properties.T,
+    command_timings: List[Properties.T],
+    ml_statistics: List[Properties.T],
+    task_statistics: List[Properties.T])
+
+  val SESSION_NAME = "\fSession.name = "
+
+  def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
+  {
+    val xml_cache = new XML.Cache()
+    def parse_lines(prfx: String): List[Properties.T] =
+      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
+
+    val session_name =
+      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
+        case None => name0
+        case Some(name) if name0 == "" || name0 == name => name
+        case Some(name) =>
+          error("Session log for " + quote(name0) + " is actually from " + quote(name))
+      }
+    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
+    val command_timings = parse_lines("\fcommand_timing = ")
+    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
+    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
+
+    Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
+  }
+}
diff -r deb4a786e6f9 -r c6160d0b0337 src/Pure/Tools/ci_api.scala
--- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 20:20:21 2016 +0200
+++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 21:11:35 2016 +0200
@@ -45,11 +45,11 @@
     session_logs: List[(String, URL)])
   {
     def read_output(): String = Url.read(output)
-    def read_log(name: String, full: Boolean): Build.Session_Log_Info =
+    def read_log(name: String, full: Boolean): Build_Log.Session_Info =
     {
       val text =
         session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
-      Build.parse_session_log(name, split_lines(text), full)
+      Build_Log.parse_session_info(name, split_lines(text), full)
     }
   }
 
diff -r deb4a786e6f9 -r c6160d0b0337 src/Pure/Tools/ml_statistics.scala
--- a/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 20:20:21 2016 +0200
+++ b/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 21:11:35 2016 +0200
@@ -25,7 +25,7 @@
   def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
     new ML_Statistics(session_name, ml_statistics)
 
-  def apply(info: Build.Session_Log_Info): ML_Statistics =
+  def apply(info: Build_Log.Session_Info): ML_Statistics =
     apply(info.session_name, info.ml_statistics)
 
   val empty = apply("", Nil)
diff -r deb4a786e6f9 -r c6160d0b0337 src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Tue Oct 04 20:20:21 2016 +0200
+++ b/src/Pure/Tools/task_statistics.scala	Tue Oct 04 21:11:35 2016 +0200
@@ -20,7 +20,7 @@
   def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
     new Task_Statistics(session_name, task_statistics)
 
-  def apply(info: Build.Session_Log_Info): Task_Statistics =
+  def apply(info: Build_Log.Session_Info): Task_Statistics =
     apply(info.session_name, info.task_statistics)
 }
 
diff -r deb4a786e6f9 -r c6160d0b0337 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Oct 04 20:20:21 2016 +0200
+++ b/src/Pure/build-jars	Tue Oct 04 21:11:35 2016 +0200
@@ -108,6 +108,7 @@
   Tools/build.scala
   Tools/build_doc.scala
   Tools/build_history.scala
+  Tools/build_log.scala
   Tools/build_stats.scala
   Tools/check_keywords.scala
   Tools/check_sources.scala