src/Tools/jEdit/src/pide_docking_framework.scala
changeset 56936 6dd8866eca69
parent 56906 408b526911f7
child 59079 12a689755c3d
     1.1 --- a/src/Tools/jEdit/src/pide_docking_framework.scala	Fri May 09 23:00:18 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/pide_docking_framework.scala	Sun May 11 20:23:08 2014 +0200
     1.3 @@ -4,16 +4,18 @@
     1.4  PIDE docking framework: "Original" with some add-ons.
     1.5  */
     1.6  
     1.7 -package org.gjt.sp.jedit.gui  // sic!
     1.8 +package isabelle.jedit
     1.9  
    1.10  
    1.11  import isabelle._
    1.12 -import isabelle.jedit._
    1.13  
    1.14  import java.awt.event.{ActionListener, ActionEvent}
    1.15  import javax.swing.{JPopupMenu, JMenuItem}
    1.16  
    1.17  import org.gjt.sp.jedit.View
    1.18 +import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
    1.19 +  DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
    1.20 +  FloatingWindowContainer, PanelWindowContainer}
    1.21  
    1.22  
    1.23  class PIDE_Docking_Framework extends DockableWindowManagerProvider