# HG changeset patch
# User wenzelm
# Date 1359044293 -3600
# Node ID 630c0895d9d1b22f0c45f8c184d2d9d1ba1a8ccd
# Parent  890f502f0e895496bec7a7f26e13728383bfd9de
more efficient inlined properties, especially relevant for voluminous tasks trace;

diff -r 890f502f0e89 -r 630c0895d9d1 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Tue Jan 22 11:28:54 2013 +0100
+++ b/src/Pure/System/session.ML	Thu Jan 24 17:18:13 2013 +0100
@@ -96,9 +96,9 @@
     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
       |> Real.fmt (StringCvt.FIX (SOME 2));
 
-    val _ =
-      writeln ("\fTiming = " ^ ML_Syntax.print_properties
-        ([("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]));
+    val timing_props =
+      [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
+    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
     val _ =
       if verbose then
         Output.physical_stderr ("Timing " ^ name ^ " (" ^
diff -r 890f502f0e89 -r 630c0895d9d1 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Jan 22 11:28:54 2013 +0100
+++ b/src/Pure/Tools/build.ML	Thu Jan 24 17:18:13 2013 +0100
@@ -14,6 +14,8 @@
 
 (* protocol messages *)
 
+local
+
 fun ML_statistics (function :: stats) "" =
       if function = Markup.ML_statistics then SOME stats
       else NONE
@@ -24,17 +26,23 @@
       else NONE
   | task_statistics _ _ = NONE;
 
+val print_properties = YXML.string_of_body o XML.Encode.properties;
+
+in
+
 fun protocol_message props output =
   (case ML_statistics props output of
-    SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
+    SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
   | NONE =>
       (case task_statistics props output of
-        SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
+        SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
       | NONE =>
           (case Markup.dest_loading_theory props of
             SOME name => writeln ("\floading_theory = " ^ name)
           | NONE => raise Fail "Undefined Output.protocol_message")));
 
+end;
+
 
 (* build *)
 
diff -r 890f502f0e89 -r 630c0895d9d1 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Jan 22 11:28:54 2013 +0100
+++ b/src/Pure/Tools/build.scala	Thu Jan 24 17:18:13 2013 +0100
@@ -521,28 +521,11 @@
   }
 
 
-  /* inlined properties -- syntax similar to ML */
+  /* inlined properties (YXML) */
 
   object Props
   {
-    private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
-
-    private object Parser extends Parse.Parser
-    {
-      def prop: Parser[Properties.Entry] =
-        keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
-        { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
-      def props: Parser[Properties.T] =
-        keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]")
-    }
-
-    def parse(text: String): Properties.T =
-    {
-      Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match {
-        case Parser.Success(result, _) => result
-        case bad => error(bad.toString)
-      }
-    }
+    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
 
     def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
       for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)