src/Tools/jEdit/src/sledgehammer_dockable.scala
changeset 57612 990ffb84489b
parent 57044 042d6e58cb40
child 60202 a95023a21725
     1.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -55,14 +55,14 @@
     1.4  
     1.5    private def handle_resize()
     1.6    {
     1.7 -    Swing_Thread.require {}
     1.8 +    GUI_Thread.require {}
     1.9  
    1.10      pretty_text_area.resize(
    1.11        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    1.12    }
    1.13  
    1.14    private val delay_resize =
    1.15 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.16 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.17  
    1.18    addComponentListener(new ComponentAdapter {
    1.19      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    1.20 @@ -135,7 +135,7 @@
    1.21  
    1.22    private val main =
    1.23      Session.Consumer[Session.Global_Options](getClass.getName) {
    1.24 -      case _: Session.Global_Options => Swing_Thread.later { update_provers(); handle_resize() }
    1.25 +      case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
    1.26      }
    1.27  
    1.28    override def init()