equal
deleted
inserted
replaced
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 PIDE docking framework: "Original" with some add-ons. |
4 PIDE docking framework: "Original" with some add-ons. |
5 */ |
5 */ |
6 |
6 |
7 package org.gjt.sp.jedit.gui // sic! |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 import isabelle.jedit._ |
|
12 |
11 |
13 import java.awt.event.{ActionListener, ActionEvent} |
12 import java.awt.event.{ActionListener, ActionEvent} |
14 import javax.swing.{JPopupMenu, JMenuItem} |
13 import javax.swing.{JPopupMenu, JMenuItem} |
15 |
14 |
16 import org.gjt.sp.jedit.View |
15 import org.gjt.sp.jedit.View |
|
16 import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory, |
|
17 DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer, |
|
18 FloatingWindowContainer, PanelWindowContainer} |
17 |
19 |
18 |
20 |
19 class PIDE_Docking_Framework extends DockableWindowManagerProvider |
21 class PIDE_Docking_Framework extends DockableWindowManagerProvider |
20 { |
22 { |
21 override def create( |
23 override def create( |