src/Pure/General/markup.scala
changeset 40848 8662b9b1f123
parent 40394 6dcb6cbf0719
child 41483 4a8431c73cf2
--- a/src/Pure/General/markup.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/General/markup.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -227,15 +227,14 @@
   {
     def apply(timing: isabelle.Timing): Markup =
       Markup(TIMING, List(
-        (ELAPSED, Double(timing.elapsed)),
-        (CPU, Double(timing.cpu)),
-        (GC, Double(timing.gc))))
+        (ELAPSED, Double(timing.elapsed.seconds)),
+        (CPU, Double(timing.cpu.seconds)),
+        (GC, Double(timing.gc.seconds))))
     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))
+          (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
+            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
   }