tolerate odd negative times from old log files (before 1698e9ccef2d);
authorwenzelm
Sat Nov 04 19:44:28 2017 +0100 (18 months ago)
changeset 67007978c584609de
parent 67006 b1278ed3cd46
child 67008 eed58245b579
tolerate odd negative times from old log files (before 1698e9ccef2d);
src/Pure/Admin/build_log.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Sat Nov 04 19:17:19 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_log.scala	Sat Nov 04 19:44:28 2017 +0100
     1.3 @@ -518,7 +518,9 @@
     1.4      object Theory_Timing
     1.5      {
     1.6        def unapply(line: String): Option[(String, (String, Timing))] =
     1.7 -        Library.try_unprefix(THEORY_TIMING_MARKER, line).map(log_file.parse_props(_)) match {
     1.8 +      {
     1.9 +        val line1 = line.replace('~', '-')
    1.10 +        Library.try_unprefix(THEORY_TIMING_MARKER, line1).map(log_file.parse_props(_)) match {
    1.11            case Some((SESSION_NAME, name) :: props) =>
    1.12              (props, props) match {
    1.13                case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t))
    1.14 @@ -526,6 +528,7 @@
    1.15              }
    1.16            case _ => None
    1.17          }
    1.18 +      }
    1.19      }
    1.20  
    1.21      var chapter = Map.empty[String, String]