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