--- 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)
}
}