src/Tools/jEdit/src/timing_dockable.scala
changeset 57612 990ffb84489b
parent 56715 52125652e82a
child 59319 677615cba30d
     1.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -145,13 +145,13 @@
     1.4    add(controls.peer, BorderLayout.NORTH)
     1.5  
     1.6  
     1.7 -  /* component state -- owned by Swing thread */
     1.8 +  /* component state -- owned by GUI thread */
     1.9  
    1.10    private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
    1.11  
    1.12    private def make_entries(): List[Entry] =
    1.13    {
    1.14 -    Swing_Thread.require {}
    1.15 +    GUI_Thread.require {}
    1.16  
    1.17      val name =
    1.18        Document_View(view.getTextArea) match {
    1.19 @@ -174,7 +174,7 @@
    1.20  
    1.21    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
    1.22    {
    1.23 -    Swing_Thread.require {}
    1.24 +    GUI_Thread.require {}
    1.25  
    1.26      val snapshot = PIDE.session.snapshot()
    1.27  
    1.28 @@ -204,7 +204,7 @@
    1.29    private val main =
    1.30      Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.31        case changed =>
    1.32 -        Swing_Thread.later { handle_update(Some(changed.nodes)) }
    1.33 +        GUI_Thread.later { handle_update(Some(changed.nodes)) }
    1.34      }
    1.35  
    1.36    override def init()