# HG changeset patch
# User wenzelm
# Date 1357735137 -3600
# Node ID a0f22c2d60ccd4f815cdd6d05a96bd11bda6cd0d
# Parent  15dc91cf47502d37c3e847d15ca7b455cbf7421f
standardized treatment of timing properties;

diff -r 15dc91cf4750 -r a0f22c2d60cc src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Wed Jan 09 12:22:09 2013 +0100
+++ b/src/Pure/General/timing.ML	Wed Jan 09 13:38:57 2013 +0100
@@ -21,7 +21,6 @@
   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
 
@@ -67,17 +66,6 @@
   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;
diff -r 15dc91cf4750 -r a0f22c2d60cc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Jan 09 12:22:09 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Jan 09 13:38:57 2013 +0100
@@ -92,6 +92,7 @@
   val elapsedN: string
   val cpuN: string
   val gcN: string
+  val timing_properties: Timing.timing -> Properties.T
   val timingN: string val timing: Timing.timing -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
@@ -323,16 +324,17 @@
 
 (* timing *)
 
-val timingN = "timing";
 val elapsedN = "elapsed";
 val cpuN = "cpu";
 val gcN = "gc";
 
-fun timing {elapsed, cpu, gc} =
-  (timingN,
-   [(elapsedN, Time.toString elapsed),
-    (cpuN, Time.toString cpu),
-    (gcN, Time.toString gc)]);
+fun timing_properties {elapsed, cpu, gc} =
+ [(elapsedN, Time.toString elapsed),
+  (cpuN, Time.toString cpu),
+  (gcN, Time.toString gc)];
+
+val timingN = "timing";
+fun timing t = (timingN, timing_properties t);
 
 
 (* toplevel *)
diff -r 15dc91cf4750 -r a0f22c2d60cc src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Jan 09 12:22:09 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Jan 09 13:38:57 2013 +0100
@@ -181,25 +181,30 @@
 
   /* timing */
 
+  val Elapsed = new Properties.Double("elapsed")
+  val CPU = new Properties.Double("cpu")
+  val GC = new Properties.Double("gc")
+
+  object Timing_Properties
+  {
+    def apply(timing: isabelle.Timing): Properties.T =
+      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
+    def unapply(props: Properties.T): Option[isabelle.Timing] =
+      (props, props, props) match {
+        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
+          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+        case _ => None
+      }
+  }
+
   val TIMING = "timing"
-  val ELAPSED = "elapsed"
-  val CPU = "cpu"
-  val GC = "gc"
 
   object Timing
   {
-    def apply(timing: isabelle.Timing): Markup =
-      Markup(TIMING, List(
-        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
-        (CPU, Properties.Value.Double(timing.cpu.seconds)),
-        (GC, Properties.Value.Double(timing.gc.seconds))))
+    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
-        case Markup(TIMING, List(
-          (ELAPSED, Properties.Value.Double(elapsed)),
-          (CPU, Properties.Value.Double(cpu)),
-          (GC, Properties.Value.Double(gc)))) =>
-            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
         case _ => None
       }
   }
diff -r 15dc91cf4750 -r a0f22c2d60cc src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Wed Jan 09 12:22:09 2013 +0100
+++ b/src/Pure/System/session.ML	Wed Jan 09 13:38:57 2013 +0100
@@ -98,7 +98,7 @@
 
     val _ =
       writeln ("\fTiming = " ^ ML_Syntax.print_properties
-        ([("threads", threads)] @ Timing.properties timing @ [("factor", factor)]));
+        ([("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]));
     val _ =
       if verbose then
         Output.physical_stderr ("Timing " ^ name ^ " (" ^