src/Pure/Tools/build_log.scala
author wenzelm
Wed Oct 05 13:56:19 2016 +0200 (2016-10-05)
changeset 64053 7ece2e14fd6c
parent 64045 c6160d0b0337
child 64054 1fc9ab31720d
permissions -rw-r--r--
more operations;
     1 /*  Title:      Pure/Tools/build_log.scala
     2     Author:     Makarius
     3 
     4 Build log parsing for historic versions, back to "build_history_base".
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Build_Log
    11 {
    12   /* inlined properties (YXML) */
    13 
    14   object Props
    15   {
    16     def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props))
    17     def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    18 
    19     def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    20       for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    21 
    22     def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    23       lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    24   }
    25 
    26 
    27   /* session log: produced by "isabelle build" */
    28 
    29   sealed case class Session_Info(
    30     session_name: String,
    31     session_timing: Properties.T,
    32     command_timings: List[Properties.T],
    33     ml_statistics: List[Properties.T],
    34     task_statistics: List[Properties.T])
    35 
    36   val SESSION_NAME = "\fSession.name = "
    37 
    38   def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    39   {
    40     val xml_cache = new XML.Cache()
    41     def parse_lines(prfx: String): List[Properties.T] =
    42       Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    43 
    44     val session_name =
    45       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
    46         case None => name0
    47         case Some(name) if name0 == "" || name0 == name => name
    48         case Some(name) =>
    49           error("Session log for " + quote(name0) + " is actually from " + quote(name))
    50       }
    51     val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    52     val command_timings = parse_lines("\fcommand_timing = ")
    53     val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    54     val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    55 
    56     Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    57   }
    58 }