src/Tools/jEdit/src/pide_docking_framework.scala
author wenzelm
Thu May 08 00:14:06 2014 +0200 (2014-05-08)
changeset 56906 408b526911f7
child 56936 6dd8866eca69
permissions -rw-r--r--
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
     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 org.gjt.sp.jedit.gui  // sic!
     8 
     9 
    10 import isabelle._
    11 import isabelle.jedit._
    12 
    13 import java.awt.event.{ActionListener, ActionEvent}
    14 import javax.swing.{JPopupMenu, JMenuItem}
    15 
    16 import org.gjt.sp.jedit.View
    17 
    18 
    19 class PIDE_Docking_Framework extends DockableWindowManagerProvider
    20 {
    21   override def create(
    22     view: View,
    23     instance: DockableWindowFactory,
    24     config: View.ViewConfig): DockableWindowManager =
    25   new DockableWindowManagerImpl(view, instance, config)
    26   {
    27     override def createPopupMenu(
    28       container: DockableWindowContainer,
    29       dockable_name: String,
    30       clone: Boolean): JPopupMenu =
    31     {
    32       val menu = super.createPopupMenu(container, dockable_name, clone)
    33 
    34       val detach_operation: Option[() => Unit] =
    35         container match {
    36           case floating: FloatingWindowContainer =>
    37             val entry = Untyped.get(floating, "entry")
    38             val win = Untyped.get(entry, "win")
    39             win match {
    40               case dockable: Dockable => dockable.detach_operation
    41               case _ => None
    42             }
    43 
    44           case panel: PanelWindowContainer =>
    45             val entries =
    46               Untyped.get(panel, "dockables").asInstanceOf[java.util.List[AnyRef]].toArray
    47             val wins =
    48               (for {
    49                 entry <- entries.iterator
    50                 if Untyped.get(Untyped.get(entry, "factory"), "name") == dockable_name
    51                 win = Untyped.get(entry, "win")
    52                 if win != null
    53               } yield win).toList
    54             wins match {
    55               case List(dockable: Dockable) => dockable.detach_operation
    56               case _ => None
    57             }
    58 
    59           case _ => None
    60         }
    61       if (detach_operation.isDefined) {
    62         val detach_item = new JMenuItem("Detach")
    63         detach_item.addActionListener(new ActionListener {
    64           def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() }
    65         })
    66         menu.add(detach_item)
    67       }
    68 
    69       menu
    70     }
    71   }
    72 }