# HG changeset patch
# User wenzelm
# Date 1504271729 -7200
# Node ID 6efa351190d089c07fa8fda7c645c910943ddbaa
# Parent  8e1aac4eed1135bd272a46ee28935af2afd4b5db
more robust: provide docking framework via base plugin;

diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 01 15:15:29 2017 +0200
@@ -20,7 +20,10 @@
 ## sources
 
 declare -a SOURCES_BASE=(
+  "src-base/dockable.scala"
   "src-base/isabelle_encoding.scala"
+  "src-base/jedit_lib.scala"
+  "src-base/pide_docking_framework.scala"
   "src-base/plugin.scala"
   "src-base/syntax_style.scala"
 )
@@ -35,7 +38,6 @@
   "src/completion_popup.scala"
   "src/context_menu.scala"
   "src/debugger_dockable.scala"
-  "src/dockable.scala"
   "src/document_model.scala"
   "src/document_view.scala"
   "src/documentation_dockable.scala"
@@ -58,7 +60,6 @@
   "src/keymap_merge.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 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src-base/dockable.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -0,0 +1,46 @@
+/*  Title:      Tools/jEdit/src-base/dockable.scala
+    Author:     Makarius
+
+Generic dockable window.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import java.awt.{Dimension, Component, BorderLayout}
+import javax.swing.JPanel
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
+
+
+class Dockable(view: View, position: String)
+  extends JPanel(new BorderLayout) with DefaultFocusComponent
+{
+  if (position == DockableWindowManager.FLOATING)
+    setPreferredSize(new Dimension(500, 250))
+
+  def focusOnDefaultComponent { JEdit_Lib.request_focus_view(view) }
+
+  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() { }
+
+  override def addNotify()
+  {
+    super.addNotify()
+    init()
+  }
+
+  override def removeNotify()
+  {
+    exit()
+    super.removeNotify()
+  }
+}
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src-base/jedit_lib.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/jedit_lib.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -0,0 +1,25 @@
+/*  Title:      Tools/jEdit/src-base/jedit_lib.scala
+    Author:     Makarius
+
+Misc library functions for jEdit.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+object JEdit_Lib
+{
+  def request_focus_view(alt_view: View = null)
+  {
+    val view = if (alt_view != null) alt_view else jEdit.getActiveView()
+    if (view != null) {
+      val text_area = view.getTextArea
+      if (text_area != null) text_area.requestFocus
+    }
+  }
+}
\ No newline at end of file
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src-base/pide_docking_framework.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -0,0 +1,71 @@
+/*  Title:      Tools/jEdit/src-base/pide_docking_framework.scala
+    Author:     Makarius
+
+PIDE docking framework: "Original" with some add-ons.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import java.awt.event.{ActionListener, ActionEvent}
+import javax.swing.{JPopupMenu, JMenuItem}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
+  DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
+  FloatingWindowContainer, PanelWindowContainer}
+
+
+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 =>
+            Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
+              case dockable: Dockable => dockable.detach_operation
+              case _ => None
+            }
+
+          case panel: PanelWindowContainer =>
+            val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
+            val wins =
+              (for {
+                entry <- entries.iterator
+                if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name
+                win = Untyped.get[Any](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 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src-base/services.xml
--- a/src/Tools/jEdit/src-base/services.xml	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src-base/services.xml	Fri Sep 01 15:15:29 2017 +0200
@@ -5,4 +5,7 @@
   <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
     new isabelle.jedit_base.Isabelle_Encoding();
   </SERVICE>
+  <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
+    new isabelle.jedit_base.PIDE_Docking_Framework();
+  </SERVICE>
 </SERVICES>
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import java.awt.{BorderLayout, Dimension}
 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/dockable.scala
--- a/src/Tools/jEdit/src/dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-/*  Title:      Tools/jEdit/src/dockable.scala
-    Author:     Makarius
-
-Generic dockable window.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.{Dimension, Component, BorderLayout}
-import javax.swing.JPanel
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
-
-
-class Dockable(view: View, position: String)
-  extends JPanel(new BorderLayout) with DefaultFocusComponent
-{
-  if (position == DockableWindowManager.FLOATING)
-    setPreferredSize(new Dimension(500, 250))
-
-  def focusOnDefaultComponent { JEdit_Lib.request_focus_view(view) }
-
-  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() { }
-
-  override def addNotify()
-  {
-    super.addNotify()
-    init()
-  }
-
-  override def removeNotify()
-  {
-    exit()
-    super.removeNotify()
-  }
-}
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import java.awt.Dimension
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import javax.swing.JComponent
 import java.awt.{Point, Font}
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -340,15 +340,6 @@
 
   /* key event handling */
 
-  def request_focus_view(alt_view: View = null)
-  {
-    val view = if (alt_view != null) alt_view else jEdit.getActiveView()
-    if (view != null) {
-      val text_area = view.getTextArea
-      if (text_area != null) text_area.requestFocus
-    }
-  }
-
   def propagate_key(view: View, evt: KeyEvent)
   {
     if (view != null && !evt.isConsumed)
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import java.awt.BorderLayout
 
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{Button, CheckBox}
 import scala.swing.event.ButtonClicked
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/pide_docking_framework.scala
--- a/src/Tools/jEdit/src/pide_docking_framework.scala	Fri Sep 01 14:58:19 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-/*  Title:      Tools/jEdit/src/pide_docking_framework.scala
-    Author:     Makarius
-
-PIDE docking framework: "Original" with some add-ons.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.event.{ActionListener, ActionEvent}
-import javax.swing.{JPopupMenu, JMenuItem}
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
-  DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
-  FloatingWindowContainer, PanelWindowContainer}
-
-
-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 =>
-            Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
-              case dockable: Dockable => dockable.detach_operation
-              case _ => None
-            }
-
-          case panel: PanelWindowContainer =>
-            val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
-            val wins =
-              (for {
-                entry <- entries.iterator
-                if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name
-                win = Untyped.get[Any](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 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -136,7 +136,7 @@
       case Some((old, _ :: rest)) =>
         rest match {
           case top :: _ => top.request_focus
-          case Nil => JEdit_Lib.request_focus_view()
+          case Nil => isabelle.jedit_base.JEdit_Lib.request_focus_view()
         }
         old.foreach(_.hide_popup)
         tip.hide_popup
@@ -153,7 +153,7 @@
     deactivate()
     if (stack.isEmpty) false
     else {
-      JEdit_Lib.request_focus_view()
+      isabelle.jedit_base.JEdit_Lib.request_focus_view()
       stack.foreach(_.hide_popup)
       stack = Nil
       true
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import java.awt.BorderLayout
 
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
 import javax.swing.{JComponent, JTextField}
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{TextArea, ScrollPane}
 
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/services.xml	Fri Sep 01 15:15:29 2017 +0200
@@ -8,9 +8,6 @@
   <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 isabelle.jedit.PIDE_Docking_Framework();
-  </SERVICE>
   <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
     new isabelle.jedit.Isabelle_Sidekick_Default();
   </SERVICE>
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{Button, CheckBox, Orientation, Separator}
 import scala.swing.event.ButtonClicked
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{Button, Component, Label, CheckBox}
 import scala.swing.event.ButtonClicked
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{Button, CheckBox}
 import scala.swing.event.ButtonClicked
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.event.{SelectionChanged, ValueChanged}
 import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{TextArea, ScrollPane}
 
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
   ScrollPane, Component, CheckBox, BorderPanel}
diff -r 8e1aac4eed11 -r 6efa351190d0 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Sep 01 14:58:19 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Sep 01 15:15:29 2017 +0200
@@ -8,6 +8,7 @@
 
 
 import isabelle._
+import isabelle.jedit_base.Dockable
 
 import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
 import scala.swing.event.{MouseClicked, ValueChanged}