src/Tools/jEdit/src/simplifier_trace_window.scala
changeset 57612 990ffb84489b
parent 57044 042d6e58cb40
child 66205 e9fa94f43a15
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  class Simplifier_Trace_Window(
     1.5    view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
     1.6  {
     1.7 -  Swing_Thread.require {}
     1.8 +  GUI_Thread.require {}
     1.9  
    1.10    private val pretty_text_area = new Pretty_Text_Area(view)
    1.11    private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
    1.12 @@ -167,7 +167,7 @@
    1.13  
    1.14    def do_paint()
    1.15    {
    1.16 -    Swing_Thread.later {
    1.17 +    GUI_Thread.later {
    1.18        pretty_text_area.resize(
    1.19          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    1.20      }
    1.21 @@ -182,7 +182,7 @@
    1.22    /* resize */
    1.23  
    1.24    private val delay_resize =
    1.25 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.26 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.27  
    1.28    peer.addComponentListener(new ComponentAdapter {
    1.29      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }