src/Tools/jEdit/src/info_dockable.scala
changeset 57612 990ffb84489b
parent 57044 042d6e58cb40
child 60750 7694aa52ad56
     1.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  object Info_Dockable
     1.6  {
     1.7 -  /* implicit arguments -- owned by Swing thread */
     1.8 +  /* implicit arguments -- owned by GUI thread */
     1.9  
    1.10    private var implicit_snapshot = Document.Snapshot.init
    1.11    private var implicit_results = Command.Results.empty
    1.12 @@ -28,7 +28,7 @@
    1.13  
    1.14    private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    1.15    {
    1.16 -    Swing_Thread.require {}
    1.17 +    GUI_Thread.require {}
    1.18  
    1.19      implicit_snapshot = snapshot
    1.20      implicit_results = results
    1.21 @@ -48,7 +48,7 @@
    1.22  
    1.23  class Info_Dockable(view: View, position: String) extends Dockable(view, position)
    1.24  {
    1.25 -  /* component state -- owned by Swing thread */
    1.26 +  /* component state -- owned by GUI thread */
    1.27  
    1.28    private val snapshot = Info_Dockable.implicit_snapshot
    1.29    private val results = Info_Dockable.implicit_results
    1.30 @@ -72,7 +72,7 @@
    1.31  
    1.32    private def handle_resize()
    1.33    {
    1.34 -    Swing_Thread.require {}
    1.35 +    GUI_Thread.require {}
    1.36  
    1.37      pretty_text_area.resize(
    1.38        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    1.39 @@ -82,7 +82,7 @@
    1.40    /* resize */
    1.41  
    1.42    private val delay_resize =
    1.43 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.44 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    1.45  
    1.46    addComponentListener(new ComponentAdapter {
    1.47      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    1.48 @@ -97,7 +97,7 @@
    1.49  
    1.50    private val main =
    1.51      Session.Consumer[Session.Global_Options](getClass.getName) {
    1.52 -      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
    1.53 +      case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
    1.54      }
    1.55  
    1.56    override def init()