tuned signature, in accordance to ML version;
authorwenzelm
Thu Apr 24 11:01:14 2014 +0200 (2014-04-24)
changeset 56691ad5d7461b370
parent 56690 69b31dc7256e
child 56692 8219a65b24e3
tuned signature, in accordance to ML version;
src/Pure/General/time.scala
src/Pure/General/timing.scala
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/General/time.scala	Thu Apr 24 10:38:14 2014 +0200
     1.2 +++ b/src/Pure/General/time.scala	Thu Apr 24 11:01:14 2014 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    def seconds(s: Double): Time = new Time((s * 1000.0).round)
     1.5    def ms(m: Long): Time = new Time(m)
     1.6    val zero: Time = ms(0)
     1.7 +  def now(): Time = ms(System.currentTimeMillis())
     1.8  
     1.9    def print_seconds(s: Double): String =
    1.10      String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    1.11 @@ -23,12 +24,18 @@
    1.12  
    1.13  final class Time private(val ms: Long) extends AnyVal
    1.14  {
    1.15 -  def + (t: Time): Time = new Time(ms + t.ms)
    1.16 -
    1.17    def seconds: Double = ms / 1000.0
    1.18  
    1.19 -  def min(t: Time): Time = if (ms < t.ms) this else t
    1.20 -  def max(t: Time): Time = if (ms > t.ms) this else t
    1.21 +  def + (t: Time): Time = new Time(ms + t.ms)
    1.22 +  def - (t: Time): Time = new Time(ms - t.ms)
    1.23 +
    1.24 +  def < (t: Time): Boolean = ms < t.ms
    1.25 +  def <= (t: Time): Boolean = ms <= t.ms
    1.26 +  def > (t: Time): Boolean = ms > t.ms
    1.27 +  def >= (t: Time): Boolean = ms >= t.ms
    1.28 +
    1.29 +  def min(t: Time): Time = if (this < t) this else t
    1.30 +  def max(t: Time): Time = if (this > t) this else t
    1.31  
    1.32    def is_zero: Boolean = ms == 0
    1.33    def is_relevant: Boolean = ms >= 1
     2.1 --- a/src/Pure/General/timing.scala	Thu Apr 24 10:38:14 2014 +0200
     2.2 +++ b/src/Pure/General/timing.scala	Thu Apr 24 11:01:14 2014 +0200
     2.3 @@ -14,11 +14,11 @@
     2.4  
     2.5    def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
     2.6      if (enabled) {
     2.7 -      val start = System.currentTimeMillis()
     2.8 +      val start = Time.now()
     2.9        val result = Exn.capture(e)
    2.10 -      val stop = System.currentTimeMillis()
    2.11 +      val stop = Time.now()
    2.12  
    2.13 -      val timing = Time.ms(stop - start)
    2.14 +      val timing = stop - start
    2.15        if (timing.is_relevant)
    2.16          System.err.println(
    2.17            (if (message == null || message.isEmpty) "" else message + ": ") +
     3.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 10:38:14 2014 +0200
     3.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 11:01:14 2014 +0200
     3.3 @@ -265,7 +265,7 @@
     3.4    {
     3.5      val this_actor = self
     3.6  
     3.7 -    var prune_next = System.currentTimeMillis() + prune_delay.ms
     3.8 +    var prune_next = Time.now() + prune_delay
     3.9  
    3.10  
    3.11      /* buffered prover messages */
    3.12 @@ -315,12 +315,12 @@
    3.13        private var changed_nodes: Set[Document.Node.Name] = Set.empty
    3.14        private var changed_commands: Set[Command] = Set.empty
    3.15  
    3.16 -      private var flush_time: Option[Long] = None
    3.17 +      private var flush_time: Option[Time] = None
    3.18  
    3.19 -      def flush_timeout: Long =
    3.20 +      def flush_timeout: Time =
    3.21          flush_time match {
    3.22 -          case None => 5000L
    3.23 -          case Some(time) => (time - System.currentTimeMillis()) max 0
    3.24 +          case None => Time.seconds(5.0)
    3.25 +          case Some(time) => (time - Time.now()) max Time.zero
    3.26          }
    3.27  
    3.28        def flush()
    3.29 @@ -341,9 +341,9 @@
    3.30            changed_nodes += command.node_name
    3.31            changed_commands += command
    3.32          }
    3.33 -        val now = System.currentTimeMillis()
    3.34 +        val now = Time.now()
    3.35          flush_time match {
    3.36 -          case None => flush_time = Some(now + output_delay.ms)
    3.37 +          case None => flush_time = Some(now + output_delay)
    3.38            case Some(time) => if (now >= time) flush()
    3.39          }
    3.40        }
    3.41 @@ -450,10 +450,10 @@
    3.42                    case _ => bad_output()
    3.43                  }
    3.44                  // FIXME separate timeout event/message!?
    3.45 -                if (prover.isDefined && System.currentTimeMillis() > prune_next) {
    3.46 +                if (prover.isDefined && Time.now() > prune_next) {
    3.47                    val old_versions = global_state.change_result(_.prune_history(prune_size))
    3.48                    if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
    3.49 -                  prune_next = System.currentTimeMillis() + prune_delay.ms
    3.50 +                  prune_next = Time.now() + prune_delay
    3.51                  }
    3.52  
    3.53                case Markup.Removed_Versions =>
    3.54 @@ -499,7 +499,7 @@
    3.55      //{{{
    3.56      var finished = false
    3.57      while (!finished) {
    3.58 -      receiveWithin(delay_commands_changed.flush_timeout) {
    3.59 +      receiveWithin(delay_commands_changed.flush_timeout.ms) {
    3.60          case TIMEOUT => delay_commands_changed.flush()
    3.61  
    3.62          case Start(name, args) if prover.isEmpty =>