isabelle: src/Pure/General/time.scala@86f9c6912965 (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)
51587 7050c4656fd8 more operations on Time, Timing; wenzelm parents: 51533 diff changeset	18	val zero: Time = ms(0)
51533 3f6280aedbcc dockable window for timing information; wenzelm parents: 50298 diff changeset	19
3f6280aedbcc dockable window for timing information; wenzelm parents: 50298 diff changeset	20	def print_seconds(s: Double): String =
3f6280aedbcc dockable window for timing information; wenzelm parents: 50298 diff changeset	21	String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
40393 2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	22	}
2bb7ec08574a somewhat more uniform timing in ML vs. Scala; wenzelm parents: diff changeset	23
56351 1c735e46acf0 simplified using "value class"; wenzelm parents: 53292 diff changeset	24	final class Time private(val ms: Long) extends AnyVal
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	25	{
51587 7050c4656fd8 more operations on Time, Timing; wenzelm parents: 51533 diff changeset	26	def + (t: Time): Time = new Time(ms + t.ms)
7050c4656fd8 more operations on Time, Timing; wenzelm parents: 51533 diff changeset	27
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	28	def seconds: Double = ms / 1000.0
40852 aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	29
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	30	def min(t: Time): Time = if (ms < t.ms) this else t
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	31	def max(t: Time): Time = if (ms > t.ms) this else t
aee98c88c587 builtin time bounds (again); wenzelm parents: 40848 diff changeset	32
53292 f567c1c7b180 option to insert unique completion immediately into buffer; wenzelm parents: 51587 diff changeset	33	def is_zero: Boolean = ms == 0
46768 46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	34	def is_relevant: Boolean = ms >= 1
46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	35
51533 3f6280aedbcc dockable window for timing information; wenzelm parents: 50298 diff changeset	36	override def toString = Time.print_seconds(seconds)
46768 46acd255810d relevant timing as in ML; wenzelm parents: 46712 diff changeset	37
40848 8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	38	def message: String = toString + "s"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	39	}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double; wenzelm parents: 40393 diff changeset	40

author	wenzelm
	Tue, 22 Apr 2014 22:15:44 +0200
changeset 56658	86f9c6912965
parent 56351	1c735e46acf0
child 56691	ad5d7461b370
permissions	-rw-r--r--