src/Pure/Tools/build_log.scala
author wenzelm
Tue Oct 04 21:11:35 2016 +0200 (2016-10-04)
changeset 64045 c6160d0b0337
child 64053 7ece2e14fd6c
permissions -rw-r--r--
clarified modules;
     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 parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    17 
    18     def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    19       for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    20 
    21     def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    22       lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    23   }
    24 
    25 
    26   /* session log: produced by "isabelle build" */
    27 
    28   sealed case class Session_Info(
    29     session_name: String,
    30     session_timing: Properties.T,
    31     command_timings: List[Properties.T],
    32     ml_statistics: List[Properties.T],
    33     task_statistics: List[Properties.T])
    34 
    35   val SESSION_NAME = "\fSession.name = "
    36 
    37   def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    38   {
    39     val xml_cache = new XML.Cache()
    40     def parse_lines(prfx: String): List[Properties.T] =
    41       Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    42 
    43     val session_name =
    44       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
    45         case None => name0
    46         case Some(name) if name0 == "" || name0 == name => name
    47         case Some(name) =>
    48           error("Session log for " + quote(name0) + " is actually from " + quote(name))
    49       }
    50     val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    51     val command_timings = parse_lines("\fcommand_timing = ")
    52     val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    53     val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    54 
    55     Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    56   }
    57 }