src/Tools/jEdit/src/pide_docking_framework.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 59079 12a689755c3d
permissions -rw-r--r--
tuned signature;
     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 }