src/Pure/Concurrent/event_timer.scala
changeset 64056 0edc966bee55
parent 56768 06388a5cfb7c
child 64370 865b39487b5d
--- a/src/Pure/Concurrent/event_timer.scala	Wed Oct 05 14:34:42 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.scala	Wed Oct 05 19:45:36 2016 +0200
@@ -11,7 +11,7 @@
 package isabelle
 
 
-import java.util.{Timer, TimerTask, Date}
+import java.util.{Timer, TimerTask, Date => JDate}
 
 
 object Event_Timer
@@ -26,7 +26,7 @@
   def request(time: Time)(event: => Unit): Request =
   {
     val task = new TimerTask { def run { event } }
-    event_timer.schedule(task, new Date(time.ms))
+    event_timer.schedule(task, new JDate(time.ms))
     new Request(time, task)
   }
 }