1.1 --- a/src/Pure/Tools/build.scala	Tue Jan 22 11:28:54 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Jan 24 17:18:13 2013 +0100
     1.3 @@ -521,28 +521,11 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* inlined properties -- syntax similar to ML */
     1.8 +  /* inlined properties (YXML) */
     1.9  
    1.10    object Props
    1.11    {
    1.12 -    private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
    1.13 -
    1.14 -    private object Parser extends Parse.Parser
    1.15 -    {
    1.16 -      def prop: Parser[Properties.Entry] =
    1.17 -        keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
    1.18 -        { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
    1.19 -      def props: Parser[Properties.T] =
    1.20 -        keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]")
    1.21 -    }
    1.22 -
    1.23 -    def parse(text: String): Properties.T =
    1.24 -    {
    1.25 -      Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match {
    1.26 -        case Parser.Success(result, _) => result
    1.27 -        case bad => error(bad.toString)
    1.28 -      }
    1.29 -    }
    1.30 +    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    1.31  
    1.32      def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    1.33        for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)