src/Tools/jEdit/src/simplifier_trace_dockable.scala
changeset 57612 990ffb84489b
parent 57593 2f7d91242b99
child 60748 6d718fda8215
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -20,9 +20,9 @@
     1.4  
     1.5  class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
     1.6  {
     1.7 -  Swing_Thread.require {}
     1.8 +  GUI_Thread.require {}
     1.9  
    1.10 -  /* component state -- owned by Swing thread */
    1.11 +  /* component state -- owned by GUI thread */
    1.12  
    1.13    private var current_snapshot = Document.State.init.snapshot()
    1.14    private var current_command = Command.empty
    1.15 @@ -37,7 +37,7 @@
    1.16    private def update_contents()
    1.17    {
    1.18  
    1.19 -    Swing_Thread.require {}
    1.20 +    GUI_Thread.require {}
    1.21  
    1.22      val snapshot = current_snapshot
    1.23      val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
    1.24 @@ -71,7 +71,7 @@
    1.25  
    1.26    private def do_paint()
    1.27    {
    1.28 -    Swing_Thread.later {
    1.29 +    GUI_Thread.later {
    1.30        text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
    1.31      }
    1.32    }
    1.33 @@ -111,21 +111,21 @@
    1.34    private val main =
    1.35      Session.Consumer[Any](getClass.getName) {
    1.36        case _: Session.Global_Options =>
    1.37 -        Swing_Thread.later { handle_resize() }
    1.38 +        GUI_Thread.later { handle_resize() }
    1.39  
    1.40        case changed: Session.Commands_Changed =>
    1.41 -        Swing_Thread.later { handle_update(do_update) }
    1.42 +        GUI_Thread.later { handle_update(do_update) }
    1.43  
    1.44        case Session.Caret_Focus =>
    1.45 -        Swing_Thread.later { handle_update(do_update) }
    1.46 +        GUI_Thread.later { handle_update(do_update) }
    1.47  
    1.48        case Simplifier_Trace.Event =>
    1.49 -        Swing_Thread.later { handle_update(do_update) }
    1.50 +        GUI_Thread.later { handle_update(do_update) }
    1.51      }
    1.52  
    1.53    override def init()
    1.54    {
    1.55 -    Swing_Thread.require {}
    1.56 +    GUI_Thread.require {}
    1.57  
    1.58      PIDE.session.global_options += main
    1.59      PIDE.session.commands_changed += main
    1.60 @@ -136,7 +136,7 @@
    1.61  
    1.62    override def exit()
    1.63    {
    1.64 -    Swing_Thread.require {}
    1.65 +    GUI_Thread.require {}
    1.66  
    1.67      PIDE.session.global_options -= main
    1.68      PIDE.session.commands_changed -= main
    1.69 @@ -149,7 +149,7 @@
    1.70    /* resize */
    1.71  
    1.72    private val delay_resize =
    1.73 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.74 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.75  
    1.76    addComponentListener(new ComponentAdapter {
    1.77      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }