# HG changeset patch
# User wenzelm
# Date 1361550249 -3600
# Node ID d8ca566b22b3e5f83c151239b458d81d7172138b
# Parent  ffd9d7f73e65125c4091f2689532283fad203296
more robust load_timings: ignore XML.Decode errors as well;

diff -r ffd9d7f73e65 -r d8ca566b22b3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Feb 22 17:02:16 2013 +0100
+++ b/src/Pure/Tools/build.scala	Fri Feb 22 17:24:09 2013 +0100
@@ -693,15 +693,22 @@
               case None => (Path.current, "")
             }
         }
+
+      def ignore_error(msg: String): (List[Properties.T], Double) =
+      {
+        java.lang.System.err.println("### Ignoring bad log file: " + path +
+          (if (msg == "") "" else "\n" + msg))
+        (Nil, 0.0)
+      }
+
       try {
         val info = parse_log(false, text)
         val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
         (info.command_timings, session_timing)
       }
       catch {
-        case ERROR(msg) =>
-          java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
-        (Nil, 0.0)
+        case ERROR(msg) => ignore_error(msg)
+        case _: XML.XML_Atom | _: XML.XML_Body => ignore_error("")
       }
     }