src/Tools/jEdit/src/info_dockable.scala
changeset 53712 ea51046be71b
parent 53711 8ce7795256e1
child 55618 995162143ef4
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 15:50:59 2013 +0200
@@ -113,14 +113,14 @@
 
   override def init()
   {
-    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main_actor
     handle_resize()
   }
 
   override def exit()
   {
-    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main_actor
     delay_resize.revoke()
   }