clarified modules;
authorwenzelm
Tue Oct 04 21:11:35 2016 +0200 (2016-10-04)
changeset 64045c6160d0b0337
parent 64044 deb4a786e6f9
child 64046 5a6a7401c48b
clarified modules;
src/Pure/Tools/build.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/ci_api.scala
src/Pure/Tools/ml_statistics.scala
src/Pure/Tools/task_statistics.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Tools/build.scala	Tue Oct 04 20:20:21 2016 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Oct 04 21:11:35 2016 +0200
     1.3 @@ -334,53 +334,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* inlined properties (YXML) */
     1.8 -
     1.9 -  object Props
    1.10 -  {
    1.11 -    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    1.12 -
    1.13 -    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    1.14 -      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    1.15 -
    1.16 -    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    1.17 -      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    1.18 -  }
    1.19 -
    1.20 -
    1.21 -  /* session log files */
    1.22 -
    1.23 -  private val SESSION_NAME = "\fSession.name = "
    1.24 -
    1.25 -  sealed case class Session_Log_Info(
    1.26 -    session_name: String,
    1.27 -    session_timing: Properties.T,
    1.28 -    command_timings: List[Properties.T],
    1.29 -    ml_statistics: List[Properties.T],
    1.30 -    task_statistics: List[Properties.T])
    1.31 -
    1.32 -  def parse_session_log(name0: String, lines: List[String], full: Boolean): Session_Log_Info =
    1.33 -  {
    1.34 -    val xml_cache = new XML.Cache()
    1.35 -    def parse_lines(prfx: String): List[Properties.T] =
    1.36 -      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    1.37 -
    1.38 -    val session_name =
    1.39 -      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
    1.40 -        case None => name0
    1.41 -        case Some(name) if name0 == "" || name0 == name => name
    1.42 -        case Some(name) =>
    1.43 -          error("Session log for " + quote(name0) + " is actually from " + quote(name))
    1.44 -      }
    1.45 -    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    1.46 -    val command_timings = parse_lines("\fcommand_timing = ")
    1.47 -    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    1.48 -    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    1.49 -
    1.50 -    Session_Log_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    1.51 -  }
    1.52 -
    1.53 -
    1.54    /* sources and heaps */
    1.55  
    1.56    private val SOURCES = "sources: "
    1.57 @@ -524,7 +477,7 @@
    1.58        }
    1.59  
    1.60        try {
    1.61 -        val info = parse_session_log(name, split_lines(text), false)
    1.62 +        val info = Build_Log.parse_session_info(name, split_lines(text), false)
    1.63          val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.64          (info.command_timings, session_timing)
    1.65        }
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/build_log.scala	Tue Oct 04 21:11:35 2016 +0200
     2.3 @@ -0,0 +1,57 @@
     2.4 +/*  Title:      Pure/Tools/build_log.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Build log parsing for historic versions, back to "build_history_base".
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Build_Log
    2.14 +{
    2.15 +  /* inlined properties (YXML) */
    2.16 +
    2.17 +  object Props
    2.18 +  {
    2.19 +    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    2.20 +
    2.21 +    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    2.22 +      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    2.23 +
    2.24 +    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    2.25 +      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    2.26 +  }
    2.27 +
    2.28 +
    2.29 +  /* session log: produced by "isabelle build" */
    2.30 +
    2.31 +  sealed case class Session_Info(
    2.32 +    session_name: String,
    2.33 +    session_timing: Properties.T,
    2.34 +    command_timings: List[Properties.T],
    2.35 +    ml_statistics: List[Properties.T],
    2.36 +    task_statistics: List[Properties.T])
    2.37 +
    2.38 +  val SESSION_NAME = "\fSession.name = "
    2.39 +
    2.40 +  def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    2.41 +  {
    2.42 +    val xml_cache = new XML.Cache()
    2.43 +    def parse_lines(prfx: String): List[Properties.T] =
    2.44 +      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    2.45 +
    2.46 +    val session_name =
    2.47 +      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
    2.48 +        case None => name0
    2.49 +        case Some(name) if name0 == "" || name0 == name => name
    2.50 +        case Some(name) =>
    2.51 +          error("Session log for " + quote(name0) + " is actually from " + quote(name))
    2.52 +      }
    2.53 +    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    2.54 +    val command_timings = parse_lines("\fcommand_timing = ")
    2.55 +    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    2.56 +    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    2.57 +
    2.58 +    Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    2.59 +  }
    2.60 +}
     3.1 --- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 20:20:21 2016 +0200
     3.2 +++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 21:11:35 2016 +0200
     3.3 @@ -45,11 +45,11 @@
     3.4      session_logs: List[(String, URL)])
     3.5    {
     3.6      def read_output(): String = Url.read(output)
     3.7 -    def read_log(name: String, full: Boolean): Build.Session_Log_Info =
     3.8 +    def read_log(name: String, full: Boolean): Build_Log.Session_Info =
     3.9      {
    3.10        val text =
    3.11          session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    3.12 -      Build.parse_session_log(name, split_lines(text), full)
    3.13 +      Build_Log.parse_session_info(name, split_lines(text), full)
    3.14      }
    3.15    }
    3.16  
     4.1 --- a/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 20:20:21 2016 +0200
     4.2 +++ b/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 21:11:35 2016 +0200
     4.3 @@ -25,7 +25,7 @@
     4.4    def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
     4.5      new ML_Statistics(session_name, ml_statistics)
     4.6  
     4.7 -  def apply(info: Build.Session_Log_Info): ML_Statistics =
     4.8 +  def apply(info: Build_Log.Session_Info): ML_Statistics =
     4.9      apply(info.session_name, info.ml_statistics)
    4.10  
    4.11    val empty = apply("", Nil)
     5.1 --- a/src/Pure/Tools/task_statistics.scala	Tue Oct 04 20:20:21 2016 +0200
     5.2 +++ b/src/Pure/Tools/task_statistics.scala	Tue Oct 04 21:11:35 2016 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4    def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
     5.5      new Task_Statistics(session_name, task_statistics)
     5.6  
     5.7 -  def apply(info: Build.Session_Log_Info): Task_Statistics =
     5.8 +  def apply(info: Build_Log.Session_Info): Task_Statistics =
     5.9      apply(info.session_name, info.task_statistics)
    5.10  }
    5.11  
     6.1 --- a/src/Pure/build-jars	Tue Oct 04 20:20:21 2016 +0200
     6.2 +++ b/src/Pure/build-jars	Tue Oct 04 21:11:35 2016 +0200
     6.3 @@ -108,6 +108,7 @@
     6.4    Tools/build.scala
     6.5    Tools/build_doc.scala
     6.6    Tools/build_history.scala
     6.7 +  Tools/build_log.scala
     6.8    Tools/build_stats.scala
     6.9    Tools/check_keywords.scala
    6.10    Tools/check_sources.scala