src/Tools/jEdit/src/font_info.scala
changeset 57612 990ffb84489b
parent 57044 042d6e58cb40
     1.1 --- a/src/Tools/jEdit/src/font_info.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/font_info.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    {
     1.5      private def change_size(change: Float => Float)
     1.6      {
     1.7 -      Swing_Thread.require {}
     1.8 +      GUI_Thread.require {}
     1.9  
    1.10        val size0 = main_size()
    1.11        val size = restrict_size(change(size0)).round
    1.12 @@ -54,9 +54,9 @@
    1.13        }
    1.14      }
    1.15  
    1.16 -    // owned by Swing thread
    1.17 +    // owned by GUI thread
    1.18      private var steps = 0
    1.19 -    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.20 +    private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.21      {
    1.22        change_size(size =>
    1.23          {