1 /* Title: Tools/jEdit/src/pide_docking_framework.scala |
|
2 Author: Makarius |
|
3 |
|
4 PIDE docking framework: "Original" with some add-ons. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.awt.event.{ActionListener, ActionEvent} |
|
13 import javax.swing.{JPopupMenu, JMenuItem} |
|
14 |
|
15 import org.gjt.sp.jedit.View |
|
16 import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory, |
|
17 DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer, |
|
18 FloatingWindowContainer, PanelWindowContainer} |
|
19 |
|
20 |
|
21 class PIDE_Docking_Framework extends DockableWindowManagerProvider |
|
22 { |
|
23 override def create( |
|
24 view: View, |
|
25 instance: DockableWindowFactory, |
|
26 config: View.ViewConfig): DockableWindowManager = |
|
27 new DockableWindowManagerImpl(view, instance, config) |
|
28 { |
|
29 override def createPopupMenu( |
|
30 container: DockableWindowContainer, |
|
31 dockable_name: String, |
|
32 clone: Boolean): JPopupMenu = |
|
33 { |
|
34 val menu = super.createPopupMenu(container, dockable_name, clone) |
|
35 |
|
36 val detach_operation: Option[() => Unit] = |
|
37 container match { |
|
38 case floating: FloatingWindowContainer => |
|
39 Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match { |
|
40 case dockable: Dockable => dockable.detach_operation |
|
41 case _ => None |
|
42 } |
|
43 |
|
44 case panel: PanelWindowContainer => |
|
45 val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray |
|
46 val wins = |
|
47 (for { |
|
48 entry <- entries.iterator |
|
49 if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name |
|
50 win = Untyped.get[Any](entry, "win") |
|
51 if win != null |
|
52 } yield win).toList |
|
53 wins match { |
|
54 case List(dockable: Dockable) => dockable.detach_operation |
|
55 case _ => None |
|
56 } |
|
57 |
|
58 case _ => None |
|
59 } |
|
60 if (detach_operation.isDefined) { |
|
61 val detach_item = new JMenuItem("Detach") |
|
62 detach_item.addActionListener(new ActionListener { |
|
63 def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() } |
|
64 }) |
|
65 menu.add(detach_item) |
|
66 } |
|
67 |
|
68 menu |
|
69 } |
|
70 } |
|
71 } |
|