1/* Title: Pure/General/timing.scala 2 Author: Makarius 3 4Support for time measurement. 5*/ 6 7package isabelle 8 9 10import java.util.Locale 11 12 13object Timing 14{ 15 val zero: Timing = Timing(Time.zero, Time.zero, Time.zero) 16 17 def timeit[A]( 18 message: String = "", 19 enabled: Boolean = true, 20 output: String => Unit = Output.warning(_))(e: => A): A = 21 { 22 if (enabled) { 23 val start = Time.now() 24 val result = Exn.capture(e) 25 val stop = Time.now() 26 27 val timing = stop - start 28 if (timing.is_relevant) { 29 output( 30 (if (message == null || message == "") "" else message + ": ") + 31 timing.message + " elapsed time") 32 } 33 34 Exn.release(result) 35 } 36 else e 37 } 38} 39 40sealed case class Timing(elapsed: Time, cpu: Time, gc: Time) 41{ 42 def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero 43 def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant 44 45 def resources: Time = cpu + gc 46 47 def factor: Option[Double] = 48 { 49 val t1 = elapsed.seconds 50 val t2 = resources.seconds 51 if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None 52 } 53 54 def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc) 55 56 def message: String = 57 elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" 58 59 def message_resources: String = 60 { 61 val factor_text = 62 factor match { 63 case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f)) 64 case None => "" 65 } 66 if (resources.seconds >= 3.0) 67 elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text 68 else 69 elapsed.message_hms + " elapsed time" + factor_text 70 } 71 72 override def toString: String = message 73 74 def json: JSON.Object.T = 75 JSON.Object("elapsed" -> elapsed.seconds, "cpu" -> cpu.seconds, "gc" -> gc.seconds) 76} 77