src/Tools/jEdit/src/rich_text_area.scala
changeset 57612 990ffb84489b
parent 56884 7de69b35bdaf
child 57857 4d86378e635f
     1.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    def robust_body[A](default: A)(body: => A): A =
     1.5    {
     1.6      try {
     1.7 -      Swing_Thread.require {}
     1.8 +      GUI_Thread.require {}
     1.9        if (buffer == text_area.getBuffer) body
    1.10        else {
    1.11          Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
    1.12 @@ -143,7 +143,7 @@
    1.13      def reset { update(None) }
    1.14    }
    1.15  
    1.16 -  // owned by Swing thread
    1.17 +  // owned by GUI thread
    1.18  
    1.19    private val highlight_area =
    1.20      new Active_Area[Color]((r: Rendering) => r.highlight _, None)