# HG changeset patch
# User wenzelm
# Date 1476386202 -7200
# Node ID 6688b9cd443b7127ea88ee372a77730a13235a68
# Parent  290b8ba96ecc5a58123cfb8cec3f1c1916523468
more robust wrt. old versions that use clear-text properties (e.g. Timing in build_history_base);

diff -r 290b8ba96ecc -r 6688b9cd443b src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Oct 13 17:34:39 2016 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu Oct 13 21:16:42 2016 +0200
@@ -185,6 +185,9 @@
     def find[A](f: String => Option[A]): Option[A] =
       lines.iterator.map(f).find(_.isDefined).map(_.get)
 
+    def find_line(marker: String): Option[String] =
+      find(Library.try_unprefix(marker, _))
+
     def find_match(regex: Regex): Option[String] =
       lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
         map(res => res.get.head)
@@ -210,13 +213,17 @@
       xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
 
     def filter_props(marker: String): List[Properties.T] =
-      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
-
-    def find_line(marker: String): Option[String] =
-      find(Library.try_unprefix(marker, _))
+      for {
+        line <- lines
+        s <- Library.try_unprefix(marker, line)
+        if YXML.detect(s)
+      } yield parse_props(s)
 
     def find_props(marker: String): Option[Properties.T] =
-      find_line(marker).map(parse_props(_))
+      find_line(marker) match {
+        case Some(text) if YXML.detect(text) => Some(parse_props(text))
+        case _ => None
+      }
 
 
     /* parse various formats */