isabelle: src/Pure/General/timing.scala@2bb7ec08574a (annotated)

40393 2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	1	/* Title: Pure/General/timing.scala
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	2	Author: Makarius
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	3
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	4	Basic support for time measurement.
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	5	*/
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	6
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	7	package isabelle
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	8
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	9
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	10	sealed case class Timing(val elapsed: Double, cpu: Double, gc: Double)
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	11	{
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	12	private def print_time(seconds: Double): String =
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	13	String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	14
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	15	def message: String =
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	16	print_time(elapsed) + "s elapsed time, " +
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	17	print_time(cpu) + "s cpu time, " +
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	18	print_time(gc) + "s GC time"
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	19	}
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	20

author	wenzelm
	Sat, 06 Nov 2010 17:55:32 +0100
changeset 40393	2bb7ec08574a
child 40848	8662b9b1f123
permissions	-rw-r--r--