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