isabelle: src/Pure/General/time.scala@ed6b40d15d1c (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
50298 1426d478ccda tuned import; wenzelm parents: 47993 diff changeset	11	import java.util.Locale
1426d478ccda tuned import; wenzelm parents: 47993 diff changeset	12
1426d478ccda tuned import; wenzelm parents: 47993 diff changeset	13
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	14	object Time
40393 2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	15	{
47993 135fd6f2dadd less warning in scala-2.10.0-M3; wenzelm parents: 46768 diff changeset	16	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	17	def ms(m: Long): Time = new Time(m)
40393 2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	18	}
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	19
46712 8650d9a95736 prefer final ADTs -- prevent ooddities; wenzelm parents: 45674 diff changeset	20	final class Time private(val ms: Long)
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	21	{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	22	def seconds: Double = ms / 1000.0
40852 aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	23
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	24	def min(t: Time): Time = if (ms < t.ms) this else t
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	25	def max(t: Time): Time = if (ms > t.ms) this else t
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	26
46768 46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	27	def is_relevant: Boolean = ms >= 1
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	override def toString =
50298 1426d478ccda tuned import; wenzelm parents: 47993 diff changeset	30	String.format(Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
46768 46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	31
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	32	def message: String = toString + "s"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	33	}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	34

author	Christian Sternagel
	Thu, 13 Dec 2012 13:11:38 +0100
changeset 50516	ed6b40d15d1c
parent 50298	1426d478ccda
child 51533	3f6280aedbcc
permissions	-rw-r--r--