src/Pure/General/timing.scala
changeset 67858 cba5c5657378
parent 65920 9e65c03e94da
child 71785 39613d6e2021
--- a/src/Pure/General/timing.scala	Wed Mar 14 16:52:16 2018 +0100
+++ b/src/Pure/General/timing.scala	Wed Mar 14 17:43:30 2018 +0100
@@ -70,4 +70,7 @@
   }
 
   override def toString: String = message
+
+  def json: JSON.Object.T =
+    JSON.Object("elapsed" -> elapsed.seconds, "cpu" -> cpu.seconds, "gc" -> gc.seconds)
 }