Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/src/font_info.scala
changeset 71704 b9a5eb0f3b43
parent 57612 990ffb84489b
child 73340 0ffcad1f6130 
--- a/src/Tools/jEdit/src/font_info.scala	Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/font_info.scala	Mon Apr 06 12:53:45 2020 +0200
@@ -56,7 +56,7 @@
 
     // owned by GUI thread
     private var steps = 0
-    private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+    private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
     {
       change_size(size =>
         {
isabelle