# HG changeset patch
# User wenzelm
# Date 1398691117 -7200
# Node ID 28d62a5b07e86f217783510fdf3ddc44b8c2b9ae
# Parent  e160ae47db942709f93c3d064e9e4aae2e35428e
more systematic delay_first discipline for change_buffer and prune_history;

diff -r e160ae47db94 -r 28d62a5b07e8 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Apr 28 14:41:49 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Apr 28 15:18:37 2014 +0200
@@ -8,8 +8,6 @@
 package isabelle
 
 
-import java.util.{Timer, TimerTask}
-
 import scala.collection.mutable
 import scala.collection.immutable.Queue
 
@@ -262,6 +260,7 @@
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Update_Options(options: Options)
+  private case object Prune_History
 
 
   /* buffered changes */
@@ -279,6 +278,7 @@
       nodes = Set.empty
       commands = Set.empty
     }
+    private val delay_flush = Simple_Thread.delay_first(output_delay) { flush() }
 
     def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
       assignment |= assign
@@ -286,14 +286,12 @@
         nodes += command.node_name
         commands += command
       }
+      delay_flush.invoke()
     }
 
-    private val timer = new Timer("change_buffer", true)
-    timer.schedule(new TimerTask { def run = flush() }, output_delay.ms, output_delay.ms)
-
     def shutdown()
     {
-      timer.cancel()
+      delay_flush.revoke()
       flush()
     }
   }
@@ -318,10 +316,10 @@
 
   /* manager thread */
 
+  private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+
   private val manager: Consumer_Thread[Any] =
   {
-    var prune_next = Time.now() + prune_delay
-
     var prover: Option[Prover] = None
 
 
@@ -429,12 +427,7 @@
                     postponed_changes.flush()
                   case _ => bad_output()
                 }
-                // FIXME separate timeout event/message!?
-                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 = Time.now() + prune_delay
-                }
+                delay_prune.invoke()
 
               case Markup.Removed_Versions =>
                 msg.text match {
@@ -512,6 +505,12 @@
               prover.get.terminate
             }
 
+          case Prune_History =>
+            if (prover.isDefined) {
+              val old_versions = global_state.change_result(_.prune_history(prune_size))
+              if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
+            }
+
           case Update_Options(options) =>
             if (prover.isDefined && is_ready) {
               prover.get.options(options)
@@ -553,6 +552,7 @@
     manager.send_wait(Stop)
     change_parser.shutdown()
     change_buffer.shutdown()
+    delay_prune.revoke()
     manager.shutdown()
     dispatcher.shutdown()
   }