| author | haftmann |
| Tue, 30 Nov 2010 17:22:59 +0100 | |
| changeset 40825 | c55ee3793712 |
| parent 40393 | 2bb7ec08574a |
| child 40848 | 8662b9b1f123 |
| permissions | -rw-r--r-- |
/* Title: Pure/General/timing.scala Author: Makarius Basic support for time measurement. */ package isabelle sealed case class Timing(val elapsed: Double, cpu: Double, gc: Double) { private def print_time(seconds: Double): String = String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef]) def message: String = print_time(elapsed) + "s elapsed time, " + print_time(cpu) + "s cpu time, " + print_time(gc) + "s GC time" }