src/Tools/jEdit/src/scala_console.scala
changeset 57612 990ffb84489b
parent 57609 943dbbbf7ad5
child 57848 f68cda7c85d4
--- a/src/Tools/jEdit/src/scala_console.scala	Wed Jul 23 11:08:24 2014 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Wed Jul 23 11:19:24 2014 +0200
@@ -57,7 +57,7 @@
   }
 
 
-  /* global state -- owned by Swing thread */
+  /* global state -- owned by GUI thread */
 
   @volatile private var interpreters = Map.empty[Console, Interpreter]
 
@@ -72,7 +72,7 @@
     {
       val s = buf.synchronized { val s = buf.toString; buf.clear; s }
       val str = UTF8.decode_permissive(s)
-      Swing_Thread.later {
+      GUI_Thread.later {
         if (global_out == null) System.out.print(str)
         else global_out.writeAttrs(null, str)
       }
@@ -124,7 +124,7 @@
   private def report_error(str: String)
   {
     if (global_console == null || global_err == null) System.err.println(str)
-    else Swing_Thread.later { global_err.print(global_console.getErrorColor, str) }
+    else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
   }
 
 
@@ -167,7 +167,7 @@
             running.change(_ => None)
             Thread.interrupted()
           }
-          Swing_Thread.later {
+          GUI_Thread.later {
             if (err != null) err.commandDone()
             out.commandDone()
           }