--- a/src/Pure/GUI/gui_thread.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/GUI/gui_thread.scala Sun Apr 05 13:05:40 2020 +0200
@@ -58,9 +58,9 @@
/* delayed events */
- def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
- Standard_Thread.delay_first(delay) { later { event } }
+ def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_first(delay) { later { event } }
- def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
- Standard_Thread.delay_last(delay) { later { event } }
+ def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_last(delay) { later { event } }
}