--- 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 =>