more robust load_timings: ignore XML.Decode errors as well;
authorwenzelm
Fri, 22 Feb 2013 17:24:09 +0100
changeset 51244 d8ca566b22b3
parent 51243 ffd9d7f73e65
child 51245 311fe56541ea
more robust load_timings: ignore XML.Decode errors as well;
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("")
       }
     }