isabelle: src/Pure/General/time.scala@b257053a4cbe (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	{
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 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
45249 b769a3a370ad class Time as abstract datatype; wenzelm parents: 44699 diff changeset	17	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
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	24	override def toString =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	25	String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	26	def message: String = toString + "s"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	27	}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	28

author	wenzelm
	Fri, 24 Feb 2012 21:36:20 +0100
changeset 46659	b257053a4cbe
parent 45674	eb65c9d17e2f
child 46712	8650d9a95736
permissions	-rw-r--r--