src/Tools/jEdit/src/font_info.scala

 
   object main_change
   {
     private def change_size(change: Float => Float)
     {
-      Swing_Thread.require {}
+      GUI_Thread.require {}
 
       val size0 = main_size()
       val size = restrict_size(change(size0)).round
       if (size != size0) {
         jEdit.setIntegerProperty("view.fontsize", size)

         jEdit.saveSettings()
         jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
       }
     }
 
-    // owned by Swing thread
+    // owned by GUI thread
     private var steps = 0
-    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+    private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
     {
       change_size(size =>
         {
           var i = size.round
           while (steps != 0 && i > 0) {