author | wenzelm |
Sat, 03 Jan 2015 22:34:18 +0100 | |
changeset 59256 | a80d2ef0b745 |
parent 59255 | db265648139c |
child 59259 | 399506ee38a5 |
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 |
59240 | 3 |
Author: Makarius |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
5 |
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
|
6 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
package isabelle.graphview |
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 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
import isabelle._ |
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 |
{ |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
19 |
def apply( |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
20 |
panel: Graph_Panel, |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
21 |
mouse_node: Option[Graph_Display.Node], |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
22 |
selected_nodes: List[Graph_Display.Node]): JPopupMenu = |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
23 |
{ |
50475 | 24 |
val visualizer = panel.visualizer |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
25 |
|
50475 | 26 |
val add_mutator = visualizer.model.Mutators.add _ |
59256 | 27 |
val current_graph = visualizer.model.current_graph |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
28 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
29 |
def filter_context( |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
30 |
nodes: List[Graph_Display.Node], 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
|
31 |
new Menu(caption) { |
59218 | 32 |
contents += |
33 |
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
|
34 |
def apply = |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
35 |
add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, 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
|
36 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
37 |
|
59218 | 38 |
contents += |
39 |
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
|
40 |
def apply = |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
41 |
add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, 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
|
42 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
43 |
|
59218 | 44 |
contents += |
45 |
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
|
46 |
def apply = |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
47 |
add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, 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
|
48 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
49 |
|
59218 | 50 |
contents += |
51 |
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
|
52 |
def apply = |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
53 |
add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, 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
|
54 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
55 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
56 |
if (edges) { |
59256 | 57 |
def degree_nodes(succs: Boolean) = |
58 |
(for { |
|
59 |
from <- nodes.iterator |
|
60 |
tos = if (succs) current_graph.imm_succs(from) else current_graph.imm_preds(from) |
|
61 |
if tos.nonEmpty |
|
62 |
} yield (from, tos)).toList.sortBy(_._1)(Graph_Display.Node.Ordering) |
|
63 |
||
64 |
val outs = degree_nodes(true) |
|
65 |
val ins = degree_nodes(false) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
66 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
67 |
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
|
68 |
contents += new Separator() |
59218 | 69 |
contents += |
70 |
new Menu("Edge") { |
|
71 |
if (outs.nonEmpty) { |
|
59247 | 72 |
contents += new MenuItem("From ...") { enabled = false } |
59256 | 73 |
for ((from, tos) <- outs) { |
59218 | 74 |
contents += |
59247 | 75 |
new Menu(quote(from.toString)) { |
76 |
contents += new MenuItem("To ...") { enabled = false } |
|
59256 | 77 |
for (to <- tos) { |
59218 | 78 |
contents += |
79 |
new MenuItem( |
|
59247 | 80 |
new Action(quote(to.toString)) { |
59218 | 81 |
def apply = |
82 |
add_mutator( |
|
59246 | 83 |
Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) |
59218 | 84 |
}) |
59256 | 85 |
} |
59218 | 86 |
} |
59256 | 87 |
} |
59218 | 88 |
} |
89 |
if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() } |
|
90 |
if (ins.nonEmpty) { |
|
59247 | 91 |
contents += new MenuItem("To ...") { enabled = false } |
59256 | 92 |
for ((to, froms) <- ins) { |
59218 | 93 |
contents += |
59247 | 94 |
new Menu(quote(to.toString)) { |
95 |
contents += new MenuItem("From ...") { enabled = false } |
|
59256 | 96 |
for (from <- froms) { |
59218 | 97 |
contents += |
98 |
new MenuItem( |
|
59247 | 99 |
new Action(quote(from.toString)) { |
59218 | 100 |
def apply = |
59221 | 101 |
add_mutator( |
59246 | 102 |
Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) |
59218 | 103 |
}) |
59256 | 104 |
} |
59218 | 105 |
} |
59256 | 106 |
} |
59218 | 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( |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
117 |
new Action("Remove all filters") { def apply = visualizer.model.Mutators(Nil) }).peer) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
118 |
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
|
119 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
120 |
if (mouse_node.isDefined) { |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
121 |
val node = mouse_node.get |
59247 | 122 |
popup.add(new MenuItem("Mouse over: " + quote(node.toString)) { 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
|
123 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
124 |
popup.add(filter_context(List(node), true, "Hide", true).peer) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
125 |
popup.add(filter_context(List(node), 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
|
126 |
|
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50463
diff
changeset
|
127 |
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
|
128 |
} |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
129 |
if (!selected_nodes.isEmpty) { |
59218 | 130 |
val text = |
59247 | 131 |
if (selected_nodes.length > 1) "multiple" |
132 |
else quote(selected_nodes.head.toString) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
133 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
134 |
popup.add(new MenuItem("Selected: " + 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
|
135 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
136 |
popup.add(filter_context(selected_nodes, true, "Hide", true).peer) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
137 |
popup.add(filter_context(selected_nodes, false, "Show only", 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 |
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
|
139 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
140 |
|
59255
db265648139c
clarified fit_to_window: floor scale within window bounds;
wenzelm
parents:
59247
diff
changeset
|
141 |
popup.add(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
|
142 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
143 |
popup |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
144 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
145 |
} |