--- 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()
}