src/Pure/Tools/build_log.scala
changeset 64045 c6160d0b0337
child 64053 7ece2e14fd6c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/build_log.scala	Tue Oct 04 21:11:35 2016 +0200
     1.3 @@ -0,0 +1,57 @@
     1.4 +/*  Title:      Pure/Tools/build_log.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Build log parsing for historic versions, back to "build_history_base".
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Build_Log
    1.14 +{
    1.15 +  /* inlined properties (YXML) */
    1.16 +
    1.17 +  object Props
    1.18 +  {
    1.19 +    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    1.20 +
    1.21 +    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    1.22 +      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    1.23 +
    1.24 +    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    1.25 +      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    1.26 +  }
    1.27 +
    1.28 +
    1.29 +  /* session log: produced by "isabelle build" */
    1.30 +
    1.31 +  sealed case class Session_Info(
    1.32 +    session_name: String,
    1.33 +    session_timing: Properties.T,
    1.34 +    command_timings: List[Properties.T],
    1.35 +    ml_statistics: List[Properties.T],
    1.36 +    task_statistics: List[Properties.T])
    1.37 +
    1.38 +  val SESSION_NAME = "\fSession.name = "
    1.39 +
    1.40 +  def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    1.41 +  {
    1.42 +    val xml_cache = new XML.Cache()
    1.43 +    def parse_lines(prfx: String): List[Properties.T] =
    1.44 +      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    1.45 +
    1.46 +    val session_name =
    1.47 +      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
    1.48 +        case None => name0
    1.49 +        case Some(name) if name0 == "" || name0 == name => name
    1.50 +        case Some(name) =>
    1.51 +          error("Session log for " + quote(name0) + " is actually from " + quote(name))
    1.52 +      }
    1.53 +    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    1.54 +    val command_timings = parse_lines("\fcommand_timing = ")
    1.55 +    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    1.56 +    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    1.57 +
    1.58 +    Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    1.59 +  }
    1.60 +}