1/*  Title:      Tools/jEdit/src-base/pide_docking_framework.scala
2    Author:     Makarius
3
4PIDE docking framework: "Original" with some add-ons.
5*/
6
7package isabelle.jedit_base
8
9
10import isabelle._
11
12import java.awt.event.{ActionListener, ActionEvent}
13import javax.swing.{JPopupMenu, JMenuItem}
14
15import org.gjt.sp.jedit.View
16import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
17  DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
18  FloatingWindowContainer, PanelWindowContainer}
19
20
21class 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}
72