# HG changeset patch
# User wenzelm
# Date 1509821068 -3600
# Node ID 978c584609ded0d1a36246b83aeb8630d14034f9
# Parent  b1278ed3cd463684c02de9373173ab028cb9b4d6
tolerate odd negative times from old log files (before 1698e9ccef2d);

diff -r b1278ed3cd46 -r 978c584609de src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Nov 04 19:17:19 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Nov 04 19:44:28 2017 +0100
@@ -518,7 +518,9 @@
     object Theory_Timing
     {
       def unapply(line: String): Option[(String, (String, Timing))] =
-        Library.try_unprefix(THEORY_TIMING_MARKER, line).map(log_file.parse_props(_)) match {
+      {
+        val line1 = line.replace('~', '-')
+        Library.try_unprefix(THEORY_TIMING_MARKER, line1).map(log_file.parse_props(_)) match {
           case Some((SESSION_NAME, name) :: props) =>
             (props, props) match {
               case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t))
@@ -526,6 +528,7 @@
             }
           case _ => None
         }
+      }
     }
 
     var chapter = Map.empty[String, String]