isabelle: src/Pure/General/time.scala@a8bad1369ada (annotated)

45674 eb65c9d17e2f clarified Time vs. Timing; wenzelm parents: 45673 diff changeset	1	/* Title: Pure/General/time.scala
45673 cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library; wenzelm parents: 45667 diff changeset	2	Module: PIDE
40393 2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	3	Author: Makarius
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	4
45674 eb65c9d17e2f clarified Time vs. Timing; wenzelm parents: 45673 diff changeset	5	Time based on milliseconds.
40393 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
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	8	package isabelle
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	9
45664 ac6e704dcd12 tuned signature (according to ML version); wenzelm parents: 45249 diff changeset	10
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	11	object Time
40393 2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	12	{
47993 135fd6f2dadd less warning in scala-2.10.0-M3; wenzelm parents: 46768 diff changeset	13	def seconds(s: Double): Time = new Time((s * 1000.0).round)
44699 5199ee17c7d7 property "tooltip-dismiss-delay" is edited in ms, not seconds; wenzelm parents: 40852 diff changeset	14	def ms(m: Long): Time = new Time(m)
40393 2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	15	}
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	16
46712 8650d9a95736 prefer final ADTs -- prevent ooddities; wenzelm parents: 45674 diff changeset	17	final class Time private(val ms: Long)
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	18	{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	19	def seconds: Double = ms / 1000.0
40852 aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	20
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	21	def min(t: Time): Time = if (ms < t.ms) this else t
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	22	def max(t: Time): Time = if (ms > t.ms) this else t
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	23
46768 46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	24	def is_relevant: Boolean = ms >= 1
46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	25
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	26	override def toString =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	27	String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
46768 46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	28
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	29	def message: String = toString + "s"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	30	}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	31

author	wenzelm
	Wed, 29 Aug 2012 12:55:41 +0200
changeset 48996	a8bad1369ada
parent 47993	135fd6f2dadd
child 50298	1426d478ccda
permissions	-rw-r--r--