--- 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)
}
--- /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)
+ }
+}
--- 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)
}
}
--- 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)
--- 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)
}
--- 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