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