src/Pure/General/time.scala
author wenzelm
Fri Nov 30 21:28:35 2012 +0100 (2012-11-30)
changeset 50298 1426d478ccda
parent 47993 135fd6f2dadd
child 51533 3f6280aedbcc
permissions -rw-r--r--
tuned import;
wenzelm@45674
     1
/*  Title:      Pure/General/time.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@40393
     3
    Author:     Makarius
wenzelm@40393
     4
wenzelm@45674
     5
Time based on milliseconds.
wenzelm@40393
     6
*/
wenzelm@40393
     7
wenzelm@40393
     8
package isabelle
wenzelm@40393
     9
wenzelm@45664
    10
wenzelm@50298
    11
import java.util.Locale
wenzelm@50298
    12
wenzelm@50298
    13
wenzelm@40848
    14
object Time
wenzelm@40393
    15
{
wenzelm@47993
    16
  def seconds(s: Double): Time = new Time((s * 1000.0).round)
wenzelm@44699
    17
  def ms(m: Long): Time = new Time(m)
wenzelm@40393
    18
}
wenzelm@40393
    19
wenzelm@46712
    20
final class Time private(val ms: Long)
wenzelm@40848
    21
{
wenzelm@40848
    22
  def seconds: Double = ms / 1000.0
wenzelm@40852
    23
wenzelm@40852
    24
  def min(t: Time): Time = if (ms < t.ms) this else t
wenzelm@40852
    25
  def max(t: Time): Time = if (ms > t.ms) this else t
wenzelm@40852
    26
wenzelm@46768
    27
  def is_relevant: Boolean = ms >= 1
wenzelm@46768
    28
wenzelm@40848
    29
  override def toString =
wenzelm@50298
    30
    String.format(Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
wenzelm@46768
    31
wenzelm@40848
    32
  def message: String = toString + "s"
wenzelm@40848
    33
}
wenzelm@40848
    34