src/Pure/PIDE/session.scala
changeset 56691 ad5d7461b370
parent 56690 69b31dc7256e
child 56704 c2f0ddd14747
     1.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 10:38:14 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 11:01:14 2014 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4    {
     1.5      val this_actor = self
     1.6  
     1.7 -    var prune_next = System.currentTimeMillis() + prune_delay.ms
     1.8 +    var prune_next = Time.now() + prune_delay
     1.9  
    1.10  
    1.11      /* buffered prover messages */
    1.12 @@ -315,12 +315,12 @@
    1.13        private var changed_nodes: Set[Document.Node.Name] = Set.empty
    1.14        private var changed_commands: Set[Command] = Set.empty
    1.15  
    1.16 -      private var flush_time: Option[Long] = None
    1.17 +      private var flush_time: Option[Time] = None
    1.18  
    1.19 -      def flush_timeout: Long =
    1.20 +      def flush_timeout: Time =
    1.21          flush_time match {
    1.22 -          case None => 5000L
    1.23 -          case Some(time) => (time - System.currentTimeMillis()) max 0
    1.24 +          case None => Time.seconds(5.0)
    1.25 +          case Some(time) => (time - Time.now()) max Time.zero
    1.26          }
    1.27  
    1.28        def flush()
    1.29 @@ -341,9 +341,9 @@
    1.30            changed_nodes += command.node_name
    1.31            changed_commands += command
    1.32          }
    1.33 -        val now = System.currentTimeMillis()
    1.34 +        val now = Time.now()
    1.35          flush_time match {
    1.36 -          case None => flush_time = Some(now + output_delay.ms)
    1.37 +          case None => flush_time = Some(now + output_delay)
    1.38            case Some(time) => if (now >= time) flush()
    1.39          }
    1.40        }
    1.41 @@ -450,10 +450,10 @@
    1.42                    case _ => bad_output()
    1.43                  }
    1.44                  // FIXME separate timeout event/message!?
    1.45 -                if (prover.isDefined && System.currentTimeMillis() > prune_next) {
    1.46 +                if (prover.isDefined && Time.now() > prune_next) {
    1.47                    val old_versions = global_state.change_result(_.prune_history(prune_size))
    1.48                    if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
    1.49 -                  prune_next = System.currentTimeMillis() + prune_delay.ms
    1.50 +                  prune_next = Time.now() + prune_delay
    1.51                  }
    1.52  
    1.53                case Markup.Removed_Versions =>
    1.54 @@ -499,7 +499,7 @@
    1.55      //{{{
    1.56      var finished = false
    1.57      while (!finished) {
    1.58 -      receiveWithin(delay_commands_changed.flush_timeout) {
    1.59 +      receiveWithin(delay_commands_changed.flush_timeout.ms) {
    1.60          case TIMEOUT => delay_commands_changed.flush()
    1.61  
    1.62          case Start(name, args) if prover.isEmpty =>