--- 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"
--- 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() { }
--- 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()
{
--- /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
+ }
+ }
+}
--- 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 */
--- 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>