include timing properties in log;
general Properties.parse operations;
tuned signature;

--- a/src/Pure/General/properties.scala	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/General/properties.scala	Tue Jan 08 21:16:51 2013 +0100
@@ -102,5 +102,34 @@
         case Some((_, value)) => Value.Double.unapply(value)
       }
   }
+
+
+  /* concrete syntax -- similar to ML */
+
+  private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
+
+  private object Parser extends Parse.Parser
+  {
+    def prop: Parser[Entry] =
+      keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
+      { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
+    def props: Parser[T] =
+      keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]")
+  }
+
+  def parse(text: java.lang.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_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] =
+    for (line <- lines if line.startsWith(prefix))
+      yield parse(line.substring(prefix.length))
+
+  def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] =
+    lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
 }
 

--- a/src/Pure/General/timing.ML	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/General/timing.ML	Tue Jan 08 21:16:51 2013 +0100
@@ -21,6 +21,7 @@
   val result: start -> timing
   val timing: ('a -> 'b) -> 'a -> timing * 'b
   val is_relevant: timing -> bool
+  val properties: timing -> Properties.T
   val message: timing -> string
 end
 
@@ -66,6 +67,17 @@
   in (result start, y) end;
 
 
+(* properties *)
+
+fun property name time =
+  [(name, Time.toString time)] handle Time.Time => [];
+
+fun properties {elapsed, cpu, gc} =
+  property "time_elapsed" elapsed @
+  property "time_cpu" cpu @
+  property "time_GC" gc;
+
+
 (* timing messages *)
 
 val min_time = Time.fromMilliseconds 1;

--- a/src/Pure/ML/ml_statistics.scala	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Tue Jan 08 21:16:51 2013 +0100
@@ -22,7 +22,7 @@
   final case class Entry(time: Double, data: Map[String, Double])
 
   def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
-  def apply(log: Path): ML_Statistics = apply(read_log(log))
+  def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
 
   val empty = apply(Nil)
 
@@ -50,37 +50,6 @@
 
   val standard_fields =
     List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
-
-
-  /* read properties from build log */
-
-  private val line_prefix = "\fML_statistics = "
-
-  private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
-
-  private object Parser extends Parse.Parser
-  {
-    private def stat: Parser[(String, String)] =
-      keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
-      { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
-    private def stats: Parser[Properties.T] =
-      keyword("[") ~> repsep(stat, keyword(",")) <~ keyword("]")
-
-    def parse_stats(s: String): Properties.T =
-    {
-      parse_all(stats, Token.reader(syntax.scan(s))) match {
-        case Success(result, _) => result
-        case bad => error(bad.toString)
-      }
-    }
-  }
-
-  def read_log(log: Path): List[Properties.T] =
-    for {
-      line <- split_lines(File.read_gzip(log))
-      if line.startsWith(line_prefix)
-      stats = line.substring(line_prefix.length)
-    } yield Parser.parse_stats(stats)
 }
 
 final class ML_Statistics private(val stats: List[Properties.T])

--- a/src/Pure/System/session.ML	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/System/session.ML	Tue Jan 08 21:16:51 2013 +0100
@@ -86,19 +86,25 @@
 
 (* use_dir *)
 
-fun with_timing _ false f x = f x
-  | with_timing item true f x =
-      let
-        val start = Timing.start ();
-        val y = f x;
-        val timing = Timing.result start;
-        val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
-          |> Real.fmt (StringCvt.FIX (SOME 2));
-        val _ =
-          Output.physical_stderr ("Timing " ^ item ^ " (" ^
-            string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
-            Timing.message timing ^ ", factor " ^ factor ^ ")\n");
-      in y end;
+fun with_timing name verbose f x =
+  let
+    val start = Timing.start ();
+    val y = f x;
+    val timing = Timing.result start;
+
+    val threads = string_of_int (Multithreading.max_threads_value ());
+    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)] @ Timing.properties timing @ [("factor", factor)]));
+    val _ =
+      if verbose then
+        Output.physical_stderr ("Timing " ^ name ^ " (" ^
+          threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
+      else ();
+  in y end;
 
 fun get_rpath rpath =
   (if rpath = "" then () else

--- a/src/Pure/Tools/build.ML	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/Tools/build.ML	Tue Jan 08 21:16:51 2013 +0100
@@ -21,8 +21,7 @@
 
 fun protocol_message props output =
   (case ML_statistics props output of
-    SOME stats =>
-      writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats)
+    SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
   | NONE => raise Fail "Undefined Output.protocol_message");
 
 

--- a/src/Pure/Tools/build.scala	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Jan 08 21:16:51 2013 +0100
@@ -509,7 +509,7 @@
   }
 
 
-  /* log files and corresponding heaps */
+  /* log files */
 
   private val LOG = Path.explode("log")
   private def log(name: String): Path = LOG + Path.basic(name)
@@ -517,6 +517,19 @@
 
   private val SESSION_PARENT_PATH = "\fSession.parent_path = "
 
+  sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
+
+  def parse_log(text: String): Log_Info =
+  {
+    val lines = split_lines(text)
+    val stats = Properties.parse_lines("\fML_statistics = ", lines)
+    val timing = Properties.find_parse_line("\fTiming = ", lines) getOrElse Nil
+    Log_Info(stats, timing)
+  }
+
+
+  /* sources and heaps */
+
   private def sources_stamp(digests: List[SHA1.Digest]): String =
     digests.map(_.toString).sorted.mkString("sources: ", " ", "")