src/Pure/Admin/build_log.scala
changeset 64196 6688b9cd443b
parent 64193 7a7e370e2523
child 64296 544481988e65
     1.1 --- a/src/Pure/Admin/build_log.scala	Thu Oct 13 17:34:39 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Thu Oct 13 21:16:42 2016 +0200
     1.3 @@ -185,6 +185,9 @@
     1.4      def find[A](f: String => Option[A]): Option[A] =
     1.5        lines.iterator.map(f).find(_.isDefined).map(_.get)
     1.6  
     1.7 +    def find_line(marker: String): Option[String] =
     1.8 +      find(Library.try_unprefix(marker, _))
     1.9 +
    1.10      def find_match(regex: Regex): Option[String] =
    1.11        lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
    1.12          map(res => res.get.head)
    1.13 @@ -210,13 +213,17 @@
    1.14        xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
    1.15  
    1.16      def filter_props(marker: String): List[Properties.T] =
    1.17 -      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
    1.18 -
    1.19 -    def find_line(marker: String): Option[String] =
    1.20 -      find(Library.try_unprefix(marker, _))
    1.21 +      for {
    1.22 +        line <- lines
    1.23 +        s <- Library.try_unprefix(marker, line)
    1.24 +        if YXML.detect(s)
    1.25 +      } yield parse_props(s)
    1.26  
    1.27      def find_props(marker: String): Option[Properties.T] =
    1.28 -      find_line(marker).map(parse_props(_))
    1.29 +      find_line(marker) match {
    1.30 +        case Some(text) if YXML.detect(text) => Some(parse_props(text))
    1.31 +        case _ => None
    1.32 +      }
    1.33  
    1.34  
    1.35      /* parse various formats */