src/Tools/jEdit/src/pide_docking_framework.scala
author wenzelm
Mon May 12 12:38:17 2014 +0200 (2014-05-12)
changeset 56939 c2ddbf327bbd
parent 56936 6dd8866eca69
child 59079 12a689755c3d
permissions -rw-r--r--
NEWS;
     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             val entry = Untyped.get(floating, "entry")
    40             val win = Untyped.get(entry, "win")
    41             win match {
    42               case dockable: Dockable => dockable.detach_operation
    43               case _ => None
    44             }
    45 
    46           case panel: PanelWindowContainer =>
    47             val entries =
    48               Untyped.get(panel, "dockables").asInstanceOf[java.util.List[AnyRef]].toArray
    49             val wins =
    50               (for {
    51                 entry <- entries.iterator
    52                 if Untyped.get(Untyped.get(entry, "factory"), "name") == dockable_name
    53                 win = Untyped.get(entry, "win")
    54                 if win != null
    55               } yield win).toList
    56             wins match {
    57               case List(dockable: Dockable) => dockable.detach_operation
    58               case _ => None
    59             }
    60 
    61           case _ => None
    62         }
    63       if (detach_operation.isDefined) {
    64         val detach_item = new JMenuItem("Detach")
    65         detach_item.addActionListener(new ActionListener {
    66           def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() }
    67         })
    68         menu.add(detach_item)
    69       }
    70 
    71       menu
    72     }
    73   }
    74 }