1.1 --- a/src/Pure/System/session.ML	Tue Jan 22 11:28:54 2013 +0100
     1.2 +++ b/src/Pure/System/session.ML	Thu Jan 24 17:18:13 2013 +0100
     1.3 @@ -96,9 +96,9 @@
     1.4      val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
     1.5        |> Real.fmt (StringCvt.FIX (SOME 2));
     1.6  
     1.7 -    val _ =
     1.8 -      writeln ("\fTiming = " ^ ML_Syntax.print_properties
     1.9 -        ([("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]));
    1.10 +    val timing_props =
    1.11 +      [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
    1.12 +    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
    1.13      val _ =
    1.14        if verbose then
    1.15          Output.physical_stderr ("Timing " ^ name ^ " (" ^

     2.1 --- a/src/Pure/Tools/build.ML	Tue Jan 22 11:28:54 2013 +0100
     2.2 +++ b/src/Pure/Tools/build.ML	Thu Jan 24 17:18:13 2013 +0100
     2.3 @@ -14,6 +14,8 @@
     2.4  
     2.5  (* protocol messages *)
     2.6  
     2.7 +local
     2.8 +
     2.9  fun ML_statistics (function :: stats) "" =
    2.10        if function = Markup.ML_statistics then SOME stats
    2.11        else NONE
    2.12 @@ -24,17 +26,23 @@
    2.13        else NONE
    2.14    | task_statistics _ _ = NONE;
    2.15  
    2.16 +val print_properties = YXML.string_of_body o XML.Encode.properties;
    2.17 +
    2.18 +in
    2.19 +
    2.20  fun protocol_message props output =
    2.21    (case ML_statistics props output of
    2.22 -    SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
    2.23 +    SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
    2.24    | NONE =>
    2.25        (case task_statistics props output of
    2.26 -        SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
    2.27 +        SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
    2.28        | NONE =>
    2.29            (case Markup.dest_loading_theory props of
    2.30              SOME name => writeln ("\floading_theory = " ^ name)
    2.31            | NONE => raise Fail "Undefined Output.protocol_message")));
    2.32  
    2.33 +end;
    2.34 +
    2.35  
    2.36  (* build *)
    2.37  

     3.1 --- a/src/Pure/Tools/build.scala	Tue Jan 22 11:28:54 2013 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Thu Jan 24 17:18:13 2013 +0100
     3.3 @@ -521,28 +521,11 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* inlined properties -- syntax similar to ML */
     3.8 +  /* inlined properties (YXML) */
     3.9  
    3.10    object Props
    3.11    {
    3.12 -    private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
    3.13 -
    3.14 -    private object Parser extends Parse.Parser
    3.15 -    {
    3.16 -      def prop: Parser[Properties.Entry] =
    3.17 -        keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
    3.18 -        { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
    3.19 -      def props: Parser[Properties.T] =
    3.20 -        keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]")
    3.21 -    }
    3.22 -
    3.23 -    def parse(text: String): Properties.T =
    3.24 -    {
    3.25 -      Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match {
    3.26 -        case Parser.Success(result, _) => result
    3.27 -        case bad => error(bad.toString)
    3.28 -      }
    3.29 -    }
    3.30 +    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    3.31  
    3.32      def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    3.33        for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)