# HG changeset patch
# User wenzelm
# Date 1454617736 -3600
# Node ID 2c76c66897fca72e0c1de06b7e586acd5faa3a15
# Parent  8bf765c9c2e54eb8d60270cfed2db5a6c5fc94a6
removed unused cancel operation;

diff -r 8bf765c9c2e5 -r 2c76c66897fc src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Thu Feb 04 21:22:53 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala	Thu Feb 04 21:28:56 2016 +0100
@@ -56,8 +56,7 @@
 
   /* delayed events */
 
-  final class Delay private [Standard_Thread](
-    first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
+  final class Delay private [Standard_Thread](first: Boolean, delay: => Time, event: => Unit)
   {
     private var running: Option[Event_Timer.Request] = None
 
@@ -73,8 +72,8 @@
     {
       val new_run =
         running match {
-          case Some(request) => if (first) false else { request.cancel; cancel(); true }
-          case None => cancel(); true
+          case Some(request) => if (first) false else { request.cancel; true }
+          case None => true
         }
       if (new_run)
         running = Some(Event_Timer.request(Time.now() + delay)(run))
@@ -83,8 +82,8 @@
     def revoke(): Unit = synchronized
     {
       running match {
-        case Some(request) => request.cancel; cancel(); running = None
-        case None => cancel()
+        case Some(request) => request.cancel; running = None
+        case None =>
       }
     }
 
@@ -94,20 +93,16 @@
         case Some(request) =>
           val alt_time = Time.now() + alt_delay
           if (request.time < alt_time && request.cancel) {
-            cancel()
             running = Some(Event_Timer.request(alt_time)(run))
           }
-          else cancel()
-        case None => cancel()
+        case None =>
       }
     }
   }
 
   // delayed event after first invocation
-  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
-    new Delay(true, delay, cancel, event)
+  def delay_first(delay: => Time)(event: => Unit): Delay = new Delay(true, delay, event)
 
   // delayed event after last invocation
-  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
-    new Delay(false, delay, cancel, event)
+  def delay_last(delay: => Time)(event: => Unit): Delay = new Delay(false, delay, event)
 }
diff -r 8bf765c9c2e5 -r 2c76c66897fc src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Thu Feb 04 21:22:53 2016 +0100
+++ b/src/Pure/GUI/gui_thread.scala	Thu Feb 04 21:28:56 2016 +0100
@@ -49,9 +49,9 @@
 
   /* delayed events */
 
-  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Standard_Thread.Delay = Standard_Thread.delay_first(delay, cancel) { later { event } }
+  def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
+    Standard_Thread.delay_first(delay) { later { event } }
 
-  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
-    : Standard_Thread.Delay = Standard_Thread.delay_last(delay, cancel) { later { event } }
+  def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
+    Standard_Thread.delay_last(delay) { later { event } }
 }