src/Pure/General/time.scala
author wenzelm
Sat, 31 Oct 2015 14:16:29 +0100
changeset 61528 053f7083b3eb
parent 57912 dd9550f84106
child 61602 a2f0f659a3c2
permissions -rw-r--r--
global start time as reference point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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)
61528
053f7083b3eb global start time as reference point;
wenzelm
parents: 57912
diff changeset
    18
  def now(): Time = ms(System.currentTimeMillis())
053f7083b3eb global start time as reference point;
wenzelm
parents: 57912
diff changeset
    19
51587
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 51533
diff changeset
    20
  val zero: Time = ms(0)
61528
053f7083b3eb global start time as reference point;
wenzelm
parents: 57912
diff changeset
    21
  val start: Time = now()
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50298
diff changeset
    22
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50298
diff changeset
    23
  def print_seconds(s: Double): String =
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50298
diff changeset
    24
    String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    25
}
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    26
56351
1c735e46acf0 simplified using "value class";
wenzelm
parents: 53292
diff changeset
    27
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
    28
{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    29
  def seconds: Double = ms / 1000.0
40852
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    30
56691
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    31
  def + (t: Time): Time = new Time(ms + t.ms)
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    32
  def - (t: Time): Time = new Time(ms - t.ms)
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    33
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    34
  def < (t: Time): Boolean = ms < t.ms
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    35
  def <= (t: Time): Boolean = ms <= t.ms
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    36
  def > (t: Time): Boolean = ms > t.ms
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    37
  def >= (t: Time): Boolean = ms >= t.ms
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    38
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    39
  def min(t: Time): Time = if (this < t) this else t
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 56351
diff changeset
    40
  def max(t: Time): Time = if (this > t) this else t
40852
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    41
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 51587
diff changeset
    42
  def is_zero: Boolean = ms == 0
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 46712
diff changeset
    43
  def is_relevant: Boolean = ms >= 1
46acd255810d relevant timing as in ML;
wenzelm
parents: 46712
diff changeset
    44
57912
wenzelm
parents: 56691
diff changeset
    45
  override def toString: String = Time.print_seconds(seconds)
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 46712
diff changeset
    46
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    47
  def message: String = toString + "s"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    48
}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    49