# HG changeset patch
# User wenzelm
# Date 1399500846 -7200
# Node ID 408b526911f70dc14ee78941f90b3eb420b37851
# Parent  fb38a767a78b130be9b965d898b830ac825fce5b
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;

diff -r fb38a767a78b -r 408b526911f7 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu May 08 00:12:22 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu May 08 00:14:06 2014 +0200
@@ -30,6 +30,7 @@
   "src/jedit_resources.scala"
   "src/monitor_dockable.scala"
   "src/output_dockable.scala"
+  "src/pide_docking_framework.scala"
   "src/plugin.scala"
   "src/pretty_text_area.scala"
   "src/pretty_tooltip.scala"
diff -r fb38a767a78b -r 408b526911f7 src/Tools/jEdit/src/dockable.scala
--- a/src/Tools/jEdit/src/dockable.scala	Thu May 08 00:12:22 2014 +0200
+++ b/src/Tools/jEdit/src/dockable.scala	Thu May 08 00:14:06 2014 +0200
@@ -27,6 +27,8 @@
   def set_content(c: Component) { add(c, BorderLayout.CENTER) }
   def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
 
+  def detach_operation: Option[() => Unit] = None
+
   protected def init() { }
   protected def exit() { }
 
diff -r fb38a767a78b -r 408b526911f7 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 00:12:22 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 00:14:06 2014 +0200
@@ -35,6 +35,8 @@
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
+  override val detach_operation = Some(() => pretty_text_area.detach)
+
 
   private def handle_resize()
   {
diff -r fb38a767a78b -r 408b526911f7 src/Tools/jEdit/src/pide_docking_framework.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/pide_docking_framework.scala	Thu May 08 00:14:06 2014 +0200
@@ -0,0 +1,72 @@
+/*  Title:      Tools/jEdit/src/pide_docking_framework.scala
+    Author:     Makarius
+
+PIDE docking framework: "Original" with some add-ons.
+*/
+
+package org.gjt.sp.jedit.gui  // sic!
+
+
+import isabelle._
+import isabelle.jedit._
+
+import java.awt.event.{ActionListener, ActionEvent}
+import javax.swing.{JPopupMenu, JMenuItem}
+
+import org.gjt.sp.jedit.View
+
+
+class PIDE_Docking_Framework extends DockableWindowManagerProvider
+{
+  override def create(
+    view: View,
+    instance: DockableWindowFactory,
+    config: View.ViewConfig): DockableWindowManager =
+  new DockableWindowManagerImpl(view, instance, config)
+  {
+    override def createPopupMenu(
+      container: DockableWindowContainer,
+      dockable_name: String,
+      clone: Boolean): JPopupMenu =
+    {
+      val menu = super.createPopupMenu(container, dockable_name, clone)
+
+      val detach_operation: Option[() => Unit] =
+        container match {
+          case floating: FloatingWindowContainer =>
+            val entry = Untyped.get(floating, "entry")
+            val win = Untyped.get(entry, "win")
+            win match {
+              case dockable: Dockable => dockable.detach_operation
+              case _ => None
+            }
+
+          case panel: PanelWindowContainer =>
+            val entries =
+              Untyped.get(panel, "dockables").asInstanceOf[java.util.List[AnyRef]].toArray
+            val wins =
+              (for {
+                entry <- entries.iterator
+                if Untyped.get(Untyped.get(entry, "factory"), "name") == dockable_name
+                win = Untyped.get(entry, "win")
+                if win != null
+              } yield win).toList
+            wins match {
+              case List(dockable: Dockable) => dockable.detach_operation
+              case _ => None
+            }
+
+          case _ => None
+        }
+      if (detach_operation.isDefined) {
+        val detach_item = new JMenuItem("Detach")
+        detach_item.addActionListener(new ActionListener {
+          def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() }
+        })
+        menu.add(detach_item)
+      }
+
+      menu
+    }
+  }
+}
diff -r fb38a767a78b -r 408b526911f7 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 00:12:22 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 00:14:06 2014 +0200
@@ -295,6 +295,8 @@
   select_operation()
   set_content(operations_pane)
 
+  override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
+
 
   /* resize */
 
diff -r fb38a767a78b -r 408b526911f7 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml	Thu May 08 00:12:22 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml	Thu May 08 00:14:06 2014 +0200
@@ -5,6 +5,9 @@
   <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
     new isabelle.jedit.Context_Menu();
   </SERVICE>
+	<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
+		new org.gjt.sp.jedit.gui.PIDE_Docking_Framework();
+	</SERVICE>
   <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
     new isabelle.jedit.Isabelle_Encoding();
   </SERVICE>