some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
authorwenzelm
Thu May 08 00:14:06 2014 +0200 (2014-05-08)
changeset 56906408b526911f7
parent 56905 fb38a767a78b
child 56907 0f3c375fd27c
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/pide_docking_framework.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/services.xml
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu May 08 00:12:22 2014 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu May 08 00:14:06 2014 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    "src/jedit_resources.scala"
     1.5    "src/monitor_dockable.scala"
     1.6    "src/output_dockable.scala"
     1.7 +  "src/pide_docking_framework.scala"
     1.8    "src/plugin.scala"
     1.9    "src/pretty_text_area.scala"
    1.10    "src/pretty_tooltip.scala"
     2.1 --- a/src/Tools/jEdit/src/dockable.scala	Thu May 08 00:12:22 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/dockable.scala	Thu May 08 00:14:06 2014 +0200
     2.3 @@ -27,6 +27,8 @@
     2.4    def set_content(c: Component) { add(c, BorderLayout.CENTER) }
     2.5    def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
     2.6  
     2.7 +  def detach_operation: Option[() => Unit] = None
     2.8 +
     2.9    protected def init() { }
    2.10    protected def exit() { }
    2.11  
     3.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 00:12:22 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 00:14:06 2014 +0200
     3.3 @@ -35,6 +35,8 @@
     3.4    val pretty_text_area = new Pretty_Text_Area(view)
     3.5    set_content(pretty_text_area)
     3.6  
     3.7 +  override val detach_operation = Some(() => pretty_text_area.detach)
     3.8 +
     3.9  
    3.10    private def handle_resize()
    3.11    {
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/src/pide_docking_framework.scala	Thu May 08 00:14:06 2014 +0200
     4.3 @@ -0,0 +1,72 @@
     4.4 +/*  Title:      Tools/jEdit/src/pide_docking_framework.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +PIDE docking framework: "Original" with some add-ons.
     4.8 +*/
     4.9 +
    4.10 +package org.gjt.sp.jedit.gui  // sic!
    4.11 +
    4.12 +
    4.13 +import isabelle._
    4.14 +import isabelle.jedit._
    4.15 +
    4.16 +import java.awt.event.{ActionListener, ActionEvent}
    4.17 +import javax.swing.{JPopupMenu, JMenuItem}
    4.18 +
    4.19 +import org.gjt.sp.jedit.View
    4.20 +
    4.21 +
    4.22 +class PIDE_Docking_Framework extends DockableWindowManagerProvider
    4.23 +{
    4.24 +  override def create(
    4.25 +    view: View,
    4.26 +    instance: DockableWindowFactory,
    4.27 +    config: View.ViewConfig): DockableWindowManager =
    4.28 +  new DockableWindowManagerImpl(view, instance, config)
    4.29 +  {
    4.30 +    override def createPopupMenu(
    4.31 +      container: DockableWindowContainer,
    4.32 +      dockable_name: String,
    4.33 +      clone: Boolean): JPopupMenu =
    4.34 +    {
    4.35 +      val menu = super.createPopupMenu(container, dockable_name, clone)
    4.36 +
    4.37 +      val detach_operation: Option[() => Unit] =
    4.38 +        container match {
    4.39 +          case floating: FloatingWindowContainer =>
    4.40 +            val entry = Untyped.get(floating, "entry")
    4.41 +            val win = Untyped.get(entry, "win")
    4.42 +            win match {
    4.43 +              case dockable: Dockable => dockable.detach_operation
    4.44 +              case _ => None
    4.45 +            }
    4.46 +
    4.47 +          case panel: PanelWindowContainer =>
    4.48 +            val entries =
    4.49 +              Untyped.get(panel, "dockables").asInstanceOf[java.util.List[AnyRef]].toArray
    4.50 +            val wins =
    4.51 +              (for {
    4.52 +                entry <- entries.iterator
    4.53 +                if Untyped.get(Untyped.get(entry, "factory"), "name") == dockable_name
    4.54 +                win = Untyped.get(entry, "win")
    4.55 +                if win != null
    4.56 +              } yield win).toList
    4.57 +            wins match {
    4.58 +              case List(dockable: Dockable) => dockable.detach_operation
    4.59 +              case _ => None
    4.60 +            }
    4.61 +
    4.62 +          case _ => None
    4.63 +        }
    4.64 +      if (detach_operation.isDefined) {
    4.65 +        val detach_item = new JMenuItem("Detach")
    4.66 +        detach_item.addActionListener(new ActionListener {
    4.67 +          def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() }
    4.68 +        })
    4.69 +        menu.add(detach_item)
    4.70 +      }
    4.71 +
    4.72 +      menu
    4.73 +    }
    4.74 +  }
    4.75 +}
     5.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 00:12:22 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 00:14:06 2014 +0200
     5.3 @@ -295,6 +295,8 @@
     5.4    select_operation()
     5.5    set_content(operations_pane)
     5.6  
     5.7 +  override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
     5.8 +
     5.9  
    5.10    /* resize */
    5.11  
     6.1 --- a/src/Tools/jEdit/src/services.xml	Thu May 08 00:12:22 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/services.xml	Thu May 08 00:14:06 2014 +0200
     6.3 @@ -5,6 +5,9 @@
     6.4    <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
     6.5      new isabelle.jedit.Context_Menu();
     6.6    </SERVICE>
     6.7 +	<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
     6.8 +		new org.gjt.sp.jedit.gui.PIDE_Docking_Framework();
     6.9 +	</SERVICE>
    6.10    <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
    6.11      new isabelle.jedit.Isabelle_Encoding();
    6.12    </SERVICE>