# HG changeset patch
# User wenzelm
# Date 1289063435 -3600
# Node ID 6dcb6cbf07190042c890ff8749b06d5e91429254
# Parent  2bb7ec08574aa7fd17d6f6c315405bb796c0c292
somewhat more uniform timing markup in ML vs. Scala;

diff -r 2bb7ec08574a -r 6dcb6cbf0719 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Nov 06 17:55:32 2010 +0100
+++ b/src/Pure/General/markup.ML	Sat Nov 06 18:10:35 2010 +0100
@@ -99,7 +99,10 @@
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
-  val timing: timing -> T
+  val elapsedN: string
+  val cpuN: string
+  val gcN: string
+  val timingN: string val timing: timing -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
@@ -306,11 +309,21 @@
 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
 
 
-(* toplevel *)
+(* timing *)
+
+val timingN = "timing";
+val elapsedN = "elapsed";
+val cpuN = "cpu";
+val gcN = "gc";
 
 fun timing ({elapsed, cpu, gc, ...}: timing) =
-  ("timing",
-    [("elapsed", Time.toString elapsed), ("cpu", Time.toString cpu), ("gc", Time.toString gc)]);
+  (timingN,
+   [(elapsedN, Time.toString elapsed),
+    (cpuN, Time.toString cpu),
+    (gcN, Time.toString gc)]);
+
+
+(* toplevel *)
 
 val subgoalsN = "subgoals";
 val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
diff -r 2bb7ec08574a -r 6dcb6cbf0719 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Nov 06 17:55:32 2010 +0100
+++ b/src/Pure/General/markup.scala	Sat Nov 06 18:10:35 2010 +0100
@@ -216,6 +216,31 @@
   val MALFORMED_SPAN = "malformed_span"
 
 
+  /* timing */
+
+  val TIMING = "timing"
+  val ELAPSED = "elapsed"
+  val CPU = "cpu"
+  val GC = "gc"
+
+  object Timing
+  {
+    def apply(timing: isabelle.Timing): Markup =
+      Markup(TIMING, List(
+        (ELAPSED, Double(timing.elapsed)),
+        (CPU, Double(timing.cpu)),
+        (GC, Double(timing.gc))))
+    def unapply(markup: Markup): Option[isabelle.Timing] =
+      markup match {
+        case Markup(TIMING, List(
+          (ELAPSED, Double(elapsed)),
+          (CPU, Double(cpu)),
+          (GC, Double(gc)))) => Some(isabelle.Timing(elapsed, cpu, gc))
+        case _ => None
+      }
+  }
+
+
   /* toplevel */
 
   val SUBGOALS = "subgoals"