# HG changeset patch
# User wenzelm
# Date 1398330074 -7200
# Node ID ad5d7461b370cc2016c5320b35aecde42c02988d
# Parent  69b31dc7256ea0bac94c3d071de0c8b4dcf2dc98
tuned signature, in accordance to ML version;

diff -r 69b31dc7256e -r ad5d7461b370 src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Thu Apr 24 10:38:14 2014 +0200
+++ b/src/Pure/General/time.scala	Thu Apr 24 11:01:14 2014 +0200
@@ -16,6 +16,7 @@
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
   def ms(m: Long): Time = new Time(m)
   val zero: Time = ms(0)
+  def now(): Time = ms(System.currentTimeMillis())
 
   def print_seconds(s: Double): String =
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
@@ -23,12 +24,18 @@
 
 final class Time private(val ms: Long) extends AnyVal
 {
-  def + (t: Time): Time = new Time(ms + t.ms)
-
   def seconds: Double = ms / 1000.0
 
-  def min(t: Time): Time = if (ms < t.ms) this else t
-  def max(t: Time): Time = if (ms > t.ms) this else t
+  def + (t: Time): Time = new Time(ms + t.ms)
+  def - (t: Time): Time = new Time(ms - t.ms)
+
+  def < (t: Time): Boolean = ms < t.ms
+  def <= (t: Time): Boolean = ms <= t.ms
+  def > (t: Time): Boolean = ms > t.ms
+  def >= (t: Time): Boolean = ms >= t.ms
+
+  def min(t: Time): Time = if (this < t) this else t
+  def max(t: Time): Time = if (this > t) this else t
 
   def is_zero: Boolean = ms == 0
   def is_relevant: Boolean = ms >= 1
diff -r 69b31dc7256e -r ad5d7461b370 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Thu Apr 24 10:38:14 2014 +0200
+++ b/src/Pure/General/timing.scala	Thu Apr 24 11:01:14 2014 +0200
@@ -14,11 +14,11 @@
 
   def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
     if (enabled) {
-      val start = System.currentTimeMillis()
+      val start = Time.now()
       val result = Exn.capture(e)
-      val stop = System.currentTimeMillis()
+      val stop = Time.now()
 
-      val timing = Time.ms(stop - start)
+      val timing = stop - start
       if (timing.is_relevant)
         System.err.println(
           (if (message == null || message.isEmpty) "" else message + ": ") +
diff -r 69b31dc7256e -r ad5d7461b370 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Apr 24 10:38:14 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 24 11:01:14 2014 +0200
@@ -265,7 +265,7 @@
   {
     val this_actor = self
 
-    var prune_next = System.currentTimeMillis() + prune_delay.ms
+    var prune_next = Time.now() + prune_delay
 
 
     /* buffered prover messages */
@@ -315,12 +315,12 @@
       private var changed_nodes: Set[Document.Node.Name] = Set.empty
       private var changed_commands: Set[Command] = Set.empty
 
-      private var flush_time: Option[Long] = None
+      private var flush_time: Option[Time] = None
 
-      def flush_timeout: Long =
+      def flush_timeout: Time =
         flush_time match {
-          case None => 5000L
-          case Some(time) => (time - System.currentTimeMillis()) max 0
+          case None => Time.seconds(5.0)
+          case Some(time) => (time - Time.now()) max Time.zero
         }
 
       def flush()
@@ -341,9 +341,9 @@
           changed_nodes += command.node_name
           changed_commands += command
         }
-        val now = System.currentTimeMillis()
+        val now = Time.now()
         flush_time match {
-          case None => flush_time = Some(now + output_delay.ms)
+          case None => flush_time = Some(now + output_delay)
           case Some(time) => if (now >= time) flush()
         }
       }
@@ -450,10 +450,10 @@
                   case _ => bad_output()
                 }
                 // FIXME separate timeout event/message!?
-                if (prover.isDefined && System.currentTimeMillis() > prune_next) {
+                if (prover.isDefined && Time.now() > prune_next) {
                   val old_versions = global_state.change_result(_.prune_history(prune_size))
                   if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
-                  prune_next = System.currentTimeMillis() + prune_delay.ms
+                  prune_next = Time.now() + prune_delay
                 }
 
               case Markup.Removed_Versions =>
@@ -499,7 +499,7 @@
     //{{{
     var finished = false
     while (!finished) {
-      receiveWithin(delay_commands_changed.flush_timeout) {
+      receiveWithin(delay_commands_changed.flush_timeout.ms) {
         case TIMEOUT => delay_commands_changed.flush()
 
         case Start(name, args) if prover.isEmpty =>