author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 66591 | 6efa351190d0 |
child 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
59079
diff
changeset
|
1 |
/* Title: Tools/jEdit/src-base/pide_docking_framework.scala |
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
3 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
4 |
PIDE docking framework: "Original" with some add-ons. |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
6 |
|
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
59079
diff
changeset
|
7 |
package isabelle.jedit_base |
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
8 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
9 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
11 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.event.{ActionListener, ActionEvent} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
13 |
import javax.swing.{JPopupMenu, JMenuItem} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
14 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.View |
56936
6dd8866eca69
more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
56906
diff
changeset
|
16 |
import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory, |
6dd8866eca69
more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
56906
diff
changeset
|
17 |
DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer, |
6dd8866eca69
more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
wenzelm
parents:
56906
diff
changeset
|
18 |
FloatingWindowContainer, PanelWindowContainer} |
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
19 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
20 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
21 |
class PIDE_Docking_Framework extends DockableWindowManagerProvider |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
22 |
{ |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
23 |
override def create( |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
24 |
view: View, |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
25 |
instance: DockableWindowFactory, |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
26 |
config: View.ViewConfig): DockableWindowManager = |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
27 |
new DockableWindowManagerImpl(view, instance, config) |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
28 |
{ |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
29 |
override def createPopupMenu( |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
30 |
container: DockableWindowContainer, |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
31 |
dockable_name: String, |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
32 |
clone: Boolean): JPopupMenu = |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
33 |
{ |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
34 |
val menu = super.createPopupMenu(container, dockable_name, clone) |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
35 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
36 |
val detach_operation: Option[() => Unit] = |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
37 |
container match { |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
38 |
case floating: FloatingWindowContainer => |
59079 | 39 |
Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match { |
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
40 |
case dockable: Dockable => dockable.detach_operation |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
41 |
case _ => None |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
42 |
} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
43 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
44 |
case panel: PanelWindowContainer => |
59079 | 45 |
val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray |
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
46 |
val wins = |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
47 |
(for { |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
48 |
entry <- entries.iterator |
59079 | 49 |
if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name |
50 |
win = Untyped.get[Any](entry, "win") |
|
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
51 |
if win != null |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
52 |
} yield win).toList |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
53 |
wins match { |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
54 |
case List(dockable: Dockable) => dockable.detach_operation |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
55 |
case _ => None |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
56 |
} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
57 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
58 |
case _ => None |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
59 |
} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
60 |
if (detach_operation.isDefined) { |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
61 |
val detach_item = new JMenuItem("Detach") |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
62 |
detach_item.addActionListener(new ActionListener { |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
63 |
def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() } |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
64 |
}) |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
65 |
menu.add(detach_item) |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
66 |
} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
67 |
|
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
68 |
menu |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
69 |
} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
70 |
} |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
diff
changeset
|
71 |
} |