src/Tools/jEdit/src/scala_console.scala
changeset 57612 990ffb84489b
parent 57609 943dbbbf7ad5
child 57848 f68cda7c85d4
     1.1 --- a/src/Tools/jEdit/src/scala_console.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* global state -- owned by Swing thread */
     1.8 +  /* global state -- owned by GUI thread */
     1.9  
    1.10    @volatile private var interpreters = Map.empty[Console, Interpreter]
    1.11  
    1.12 @@ -72,7 +72,7 @@
    1.13      {
    1.14        val s = buf.synchronized { val s = buf.toString; buf.clear; s }
    1.15        val str = UTF8.decode_permissive(s)
    1.16 -      Swing_Thread.later {
    1.17 +      GUI_Thread.later {
    1.18          if (global_out == null) System.out.print(str)
    1.19          else global_out.writeAttrs(null, str)
    1.20        }
    1.21 @@ -124,7 +124,7 @@
    1.22    private def report_error(str: String)
    1.23    {
    1.24      if (global_console == null || global_err == null) System.err.println(str)
    1.25 -    else Swing_Thread.later { global_err.print(global_console.getErrorColor, str) }
    1.26 +    else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
    1.27    }
    1.28  
    1.29  
    1.30 @@ -167,7 +167,7 @@
    1.31              running.change(_ => None)
    1.32              Thread.interrupted()
    1.33            }
    1.34 -          Swing_Thread.later {
    1.35 +          GUI_Thread.later {
    1.36              if (err != null) err.commandDone()
    1.37              out.commandDone()
    1.38            }