author | wenzelm |
Thu, 01 Jan 2015 11:37:09 +0100 | |
changeset 59218 | eadd82d440b0 |
parent 59202 | 711c2446dc9d |
child 59221 | f779f83ef4ec |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/popups.scala |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
3 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
PopupMenu generation for graph components. |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
5 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
9 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
10 |
import isabelle._ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
import isabelle.graphview.Mutators._ |
55618 | 12 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
13 |
import javax.swing.JPopupMenu |
49558 | 14 |
import scala.swing.{Action, Menu, MenuItem, Separator} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
|
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
17 |
object Popups |
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
18 |
{ |
59218 | 19 |
def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String]): JPopupMenu = |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
20 |
{ |
50475 | 21 |
val visualizer = panel.visualizer |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
22 |
|
50475 | 23 |
val add_mutator = visualizer.model.Mutators.add _ |
24 |
val curr = visualizer.model.current |
|
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
25 |
|
59218 | 26 |
def filter_context(ls: List[String], reverse: Boolean, caption: String, edges: Boolean) = |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
27 |
new Menu(caption) { |
59218 | 28 |
contents += |
29 |
new MenuItem(new Action("This") { |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
30 |
def apply = |
59218 | 31 |
add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, false, false))) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
32 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
33 |
|
59218 | 34 |
contents += |
35 |
new MenuItem(new Action("Family") { |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
36 |
def apply = |
59218 | 37 |
add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, true, true))) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
38 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
39 |
|
59218 | 40 |
contents += |
41 |
new MenuItem(new Action("Parents") { |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
42 |
def apply = |
59218 | 43 |
add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, false, true))) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
44 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
45 |
|
59218 | 46 |
contents += |
47 |
new MenuItem(new Action("Children") { |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
48 |
def apply = |
59218 | 49 |
add_mutator(Mutators.create(visualizer, Node_List(ls, reverse, true, false))) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
50 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
51 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
52 |
if (edges) { |
59218 | 53 |
val outs = |
54 |
ls.map(l => (l, curr.imm_succs(l))) // FIXME iterator |
|
55 |
.filter(_._2.size > 0).sortBy(_._1) |
|
56 |
val ins = |
|
57 |
ls.map(l => (l, curr.imm_preds(l))) // FIXME iterator |
|
58 |
.filter(_._2.size > 0).sortBy(_._1) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
59 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
60 |
if (outs.nonEmpty || ins.nonEmpty) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
61 |
contents += new Separator() |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
62 |
|
59218 | 63 |
contents += |
64 |
new Menu("Edge") { |
|
65 |
if (outs.nonEmpty) { |
|
66 |
contents += new MenuItem("From...") { enabled = false } |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
67 |
|
59218 | 68 |
outs.map(e => { |
69 |
val (from, tos) = e |
|
70 |
contents += |
|
71 |
new Menu(from) { |
|
72 |
contents += new MenuItem("To...") { enabled = false } |
|
73 |
||
74 |
tos.toList.sorted.distinct.map(to => { |
|
75 |
contents += |
|
76 |
new MenuItem( |
|
77 |
new Action(to) { |
|
78 |
def apply = |
|
79 |
add_mutator( |
|
80 |
Mutators.create(visualizer, Edge_Endpoints(from, to)) |
|
81 |
) |
|
82 |
}) |
|
83 |
}) |
|
84 |
} |
|
85 |
}) |
|
86 |
} |
|
87 |
if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() } |
|
88 |
if (ins.nonEmpty) { |
|
89 |
contents += new MenuItem("To...") { enabled = false } |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
90 |
|
59218 | 91 |
ins.map(e => { |
92 |
val (to, froms) = e |
|
93 |
contents += |
|
94 |
new Menu(to) { |
|
95 |
contents += new MenuItem("From...") { enabled = false } |
|
96 |
||
97 |
froms.toList.sorted.distinct.map(from => { |
|
98 |
contents += |
|
99 |
new MenuItem( |
|
100 |
new Action(from) { |
|
101 |
def apply = |
|
102 |
add_mutator(Mutators.create(visualizer, Edge_Endpoints(from, to))) |
|
103 |
}) |
|
104 |
}) |
|
105 |
} |
|
106 |
}) |
|
107 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
108 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
109 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
110 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
111 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
112 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
113 |
val popup = new JPopupMenu() |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
114 |
|
59218 | 115 |
popup.add( |
116 |
new MenuItem( |
|
117 |
new Action("Remove all filters") { |
|
50475 | 118 |
def apply = visualizer.model.Mutators(Nil) |
59218 | 119 |
}).peer) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
120 |
popup.add(new JPopupMenu.Separator) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
121 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
122 |
if (under_mouse.isDefined) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
123 |
val v = under_mouse.get |
59218 | 124 |
popup.add( |
125 |
new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) { enabled = false }.peer) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
126 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
127 |
popup.add(filter_context(List(v), true, "Hide", true).peer) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
128 |
popup.add(filter_context(List(v), false, "Show only", false).peer) |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
129 |
|
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
130 |
popup.add(new JPopupMenu.Separator) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
131 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
132 |
if (!selected.isEmpty) { |
59218 | 133 |
val text = |
134 |
if (selected.length > 1) "Multiple" |
|
135 |
else visualizer.Caption(selected.head) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
136 |
|
59218 | 137 |
popup.add(new MenuItem("Selected: %s".format(text)) { enabled = false }.peer) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
138 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
139 |
popup.add(filter_context(selected, true, "Hide", true).peer) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
140 |
popup.add(filter_context(selected, false, "Show only", false).peer) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
141 |
popup.add(new JPopupMenu.Separator) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
142 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
143 |
|
59218 | 144 |
popup.add( |
145 |
new MenuItem(new Action("Fit to Window") { def apply = panel.fit_to_window() }).peer) |
|
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
146 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
147 |
popup |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
148 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
149 |
} |