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