1 /* Title: Tools/Graphview/src/mutator_dialog.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Mutator selection and configuration dialog. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.awt.Color |
|
13 import java.awt.FocusTraversalPolicy |
|
14 import javax.swing.JColorChooser |
|
15 import javax.swing.border.EmptyBorder |
|
16 import scala.collection.JavaConversions._ |
|
17 import scala.swing._ |
|
18 import isabelle.graphview.Mutators._ |
|
19 import scala.swing.event.ValueChanged |
|
20 |
|
21 |
|
22 class Mutator_Dialog( |
|
23 visualizer: Visualizer, |
|
24 container: Mutator_Container, |
|
25 caption: String, |
|
26 reverse_caption: String = "Inverse", |
|
27 show_color_chooser: Boolean = true) |
|
28 extends Dialog |
|
29 { |
|
30 type Mutator_Markup = (Boolean, Color, Mutator) |
|
31 |
|
32 title = caption |
|
33 |
|
34 private var _panels: List[Mutator_Panel] = Nil |
|
35 private def panels = _panels |
|
36 private def panels_= (panels: List[Mutator_Panel]) { |
|
37 _panels = panels |
|
38 paintPanels |
|
39 } |
|
40 |
|
41 container.events += { |
|
42 case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m)) |
|
43 case Mutator_Event.NewList(ms) => panels = getPanels(ms) |
|
44 } |
|
45 |
|
46 override def open() { |
|
47 if (!visible) |
|
48 panels = getPanels(container()) |
|
49 |
|
50 super.open |
|
51 } |
|
52 |
|
53 minimumSize = new Dimension(700, 200) |
|
54 preferredSize = new Dimension(1000, 300) |
|
55 peer.setFocusTraversalPolicy(focusTraversal) |
|
56 |
|
57 private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] = |
|
58 m.filter(_ match {case (_, _, Identity()) => false; case _ => true}) |
|
59 .map(m => new Mutator_Panel(m)) |
|
60 |
|
61 private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = |
|
62 panels.map(panel => panel.get_Mutator_Markup) |
|
63 |
|
64 private def movePanelUp(m: Mutator_Panel) = { |
|
65 def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { |
|
66 case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs) |
|
67 case _ => l |
|
68 } |
|
69 |
|
70 panels = moveUp(panels) |
|
71 } |
|
72 |
|
73 private def movePanelDown(m: Mutator_Panel) = { |
|
74 def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { |
|
75 case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs) |
|
76 case _ => l |
|
77 } |
|
78 |
|
79 panels = moveDown(panels) |
|
80 } |
|
81 |
|
82 private def removePanel(m: Mutator_Panel) = { |
|
83 panels = panels.filter(_ != m).toList |
|
84 } |
|
85 |
|
86 private def addPanel(m: Mutator_Panel) = { |
|
87 panels = panels ::: List(m) |
|
88 } |
|
89 |
|
90 def paintPanels = { |
|
91 focusTraversal.clear |
|
92 filterPanel.contents.clear |
|
93 panels.map(x => { |
|
94 filterPanel.contents += x |
|
95 focusTraversal.addAll(x.focusList) |
|
96 }) |
|
97 filterPanel.contents += Swing.VGlue |
|
98 |
|
99 focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component]) |
|
100 focusTraversal.add(addButton.peer) |
|
101 focusTraversal.add(applyButton.peer) |
|
102 focusTraversal.add(cancelButton.peer) |
|
103 filterPanel.revalidate |
|
104 filterPanel.repaint |
|
105 } |
|
106 |
|
107 val filterPanel = new BoxPanel(Orientation.Vertical) {} |
|
108 |
|
109 private val mutatorBox = new ComboBox[Mutator](container.available) |
|
110 |
|
111 private val addButton: Button = new Button{ |
|
112 action = Action("Add") { |
|
113 addPanel( |
|
114 new Mutator_Panel((true, visualizer.Colors.next, |
|
115 mutatorBox.selection.item)) |
|
116 ) |
|
117 } |
|
118 } |
|
119 |
|
120 private val applyButton = new Button{ |
|
121 action = Action("Apply") { |
|
122 container(getMutators(panels)) |
|
123 } |
|
124 } |
|
125 |
|
126 private val resetButton = new Button { |
|
127 action = Action("Reset") { |
|
128 panels = getPanels(container()) |
|
129 } |
|
130 } |
|
131 |
|
132 private val cancelButton = new Button{ |
|
133 action = Action("Close") { |
|
134 close |
|
135 } |
|
136 } |
|
137 defaultButton = cancelButton |
|
138 |
|
139 private val botPanel = new BoxPanel(Orientation.Horizontal) { |
|
140 border = new EmptyBorder(10, 0, 0, 0) |
|
141 |
|
142 contents += mutatorBox |
|
143 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
144 contents += addButton |
|
145 |
|
146 contents += Swing.HGlue |
|
147 contents += Swing.RigidBox(new Dimension(30, 0)) |
|
148 contents += applyButton |
|
149 |
|
150 contents += Swing.RigidBox(new Dimension(5, 0)) |
|
151 contents += resetButton |
|
152 |
|
153 contents += Swing.RigidBox(new Dimension(5, 0)) |
|
154 contents += cancelButton |
|
155 } |
|
156 |
|
157 contents = new BorderPanel { |
|
158 border = new EmptyBorder(5, 5, 5, 5) |
|
159 |
|
160 add(new ScrollPane(filterPanel), BorderPanel.Position.Center) |
|
161 add(botPanel, BorderPanel.Position.South) |
|
162 } |
|
163 |
|
164 private class Mutator_Panel(initials: Mutator_Markup) |
|
165 extends BoxPanel(Orientation.Horizontal) |
|
166 { |
|
167 private val (_enabled, _color, _mutator) = initials |
|
168 |
|
169 private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs() |
|
170 var focusList = List.empty[java.awt.Component] |
|
171 private val enabledBox = new iCheckBox("Enabled", _enabled) |
|
172 |
|
173 border = new EmptyBorder(5, 5, 5, 5) |
|
174 maximumSize = new Dimension(Integer.MAX_VALUE, 30) |
|
175 background = _color |
|
176 |
|
177 contents += new Label(_mutator.name) { |
|
178 preferredSize = new Dimension(175, 20) |
|
179 horizontalAlignment = Alignment.Left |
|
180 if (_mutator.description != "") tooltip = _mutator.description |
|
181 } |
|
182 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
183 contents += enabledBox |
|
184 contents += Swing.RigidBox(new Dimension(5, 0)) |
|
185 focusList = enabledBox.peer :: focusList |
|
186 inputs.map( _ match { |
|
187 case (n, c) => { |
|
188 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
189 if (n != "") { |
|
190 contents += new Label(n) |
|
191 contents += Swing.RigidBox(new Dimension(5, 0)) |
|
192 } |
|
193 contents += c.asInstanceOf[Component] |
|
194 |
|
195 focusList = c.asInstanceOf[Component].peer :: focusList |
|
196 } |
|
197 case _ => |
|
198 }) |
|
199 |
|
200 { |
|
201 val t = this |
|
202 contents += Swing.HGlue |
|
203 contents += Swing.RigidBox(new Dimension(10, 0)) |
|
204 |
|
205 if (show_color_chooser) { |
|
206 contents += new Button { |
|
207 maximumSize = new Dimension(20, 20) |
|
208 |
|
209 action = Action("Color") { |
|
210 t.background = |
|
211 JColorChooser.showDialog(t.peer, "Choose new Color", t.background) |
|
212 } |
|
213 |
|
214 focusList = this.peer :: focusList |
|
215 } |
|
216 contents += Swing.RigidBox(new Dimension(2, 0)) |
|
217 } |
|
218 |
|
219 contents += new Button { |
|
220 maximumSize = new Dimension(20, 20) |
|
221 |
|
222 action = Action("Up") { |
|
223 movePanelUp(t) |
|
224 } |
|
225 |
|
226 focusList = this.peer :: focusList |
|
227 } |
|
228 contents += Swing.RigidBox(new Dimension(2, 0)) |
|
229 contents += new Button { |
|
230 maximumSize = new Dimension(20, 20) |
|
231 |
|
232 action = Action("Down") { |
|
233 movePanelDown(t) |
|
234 } |
|
235 |
|
236 focusList = this.peer :: focusList |
|
237 } |
|
238 contents += Swing.RigidBox(new Dimension(2, 0)) |
|
239 contents += new Button { |
|
240 maximumSize = new Dimension(20, 20) |
|
241 |
|
242 action = Action("Del") { |
|
243 removePanel(t) |
|
244 } |
|
245 |
|
246 focusList = this.peer :: focusList |
|
247 } |
|
248 } |
|
249 |
|
250 focusList = focusList.reverse |
|
251 |
|
252 private def isRegex(regex: String): Boolean = { |
|
253 try { |
|
254 regex.r |
|
255 |
|
256 true |
|
257 } catch { |
|
258 case _: java.util.regex.PatternSyntaxException => false |
|
259 } |
|
260 } |
|
261 |
|
262 def get_Mutator_Markup: Mutator_Markup = { |
|
263 def regexOrElse(regex: String, orElse: String): String = { |
|
264 if (isRegex(regex)) regex |
|
265 else orElse |
|
266 } |
|
267 |
|
268 val m = _mutator match { |
|
269 case Identity() => |
|
270 Identity() |
|
271 case Node_Expression(r, _, _, _) => |
|
272 Node_Expression( |
|
273 regexOrElse(inputs(2)._2.getString, r), |
|
274 inputs(3)._2.getBool, |
|
275 // "Parents" means "Show parents" or "Matching Children" |
|
276 inputs(1)._2.getBool, |
|
277 inputs(0)._2.getBool |
|
278 ) |
|
279 case Node_List(_, _, _, _) => |
|
280 Node_List( |
|
281 inputs(2)._2.getString.split(',').filter(_ != "").toList, |
|
282 inputs(3)._2.getBool, |
|
283 // "Parents" means "Show parents" or "Matching Children" |
|
284 inputs(1)._2.getBool, |
|
285 inputs(0)._2.getBool |
|
286 ) |
|
287 case Edge_Endpoints(_, _) => |
|
288 Edge_Endpoints( |
|
289 inputs(0)._2.getString, |
|
290 inputs(1)._2.getString |
|
291 ) |
|
292 case Add_Node_Expression(r) => |
|
293 Add_Node_Expression( |
|
294 regexOrElse(inputs(0)._2.getString, r) |
|
295 ) |
|
296 case Add_Transitive_Closure(_, _) => |
|
297 Add_Transitive_Closure( |
|
298 inputs(0)._2.getBool, |
|
299 inputs(1)._2.getBool |
|
300 ) |
|
301 case _ => |
|
302 Identity() |
|
303 } |
|
304 |
|
305 (enabledBox.selected, background, m) |
|
306 } |
|
307 |
|
308 private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match { |
|
309 case Node_Expression(regex, reverse, check_parents, check_children) => |
|
310 List( |
|
311 ("", new iCheckBox("Parents", check_children)), |
|
312 ("", new iCheckBox("Children", check_parents)), |
|
313 ("Regex", new iTextField(regex, x => !isRegex(x))), |
|
314 ("", new iCheckBox(reverse_caption, reverse)) |
|
315 ) |
|
316 case Node_List(list, reverse, check_parents, check_children) => |
|
317 List( |
|
318 ("", new iCheckBox("Parents", check_children)), |
|
319 ("", new iCheckBox("Children", check_parents)), |
|
320 ("Names", new iTextField(list.mkString(","))), |
|
321 ("", new iCheckBox(reverse_caption, reverse)) |
|
322 ) |
|
323 case Edge_Endpoints(source, dest) => |
|
324 List( |
|
325 ("Source", new iTextField(source)), |
|
326 ("Destination", new iTextField(dest)) |
|
327 ) |
|
328 case Add_Node_Expression(regex) => |
|
329 List( |
|
330 ("Regex", new iTextField(regex, x => !isRegex(x))) |
|
331 ) |
|
332 case Add_Transitive_Closure(parents, children) => |
|
333 List( |
|
334 ("", new iCheckBox("Parents", parents)), |
|
335 ("", new iCheckBox("Children", children)) |
|
336 ) |
|
337 case _ => Nil |
|
338 } |
|
339 } |
|
340 |
|
341 private trait Mutator_Input_Value |
|
342 { |
|
343 def getString: String |
|
344 def getBool: Boolean |
|
345 } |
|
346 |
|
347 private class iTextField(t: String, colorator: String => Boolean) |
|
348 extends TextField(t) with Mutator_Input_Value |
|
349 { |
|
350 def this(t: String) = this(t, x => false) |
|
351 |
|
352 preferredSize = new Dimension(125, 18) |
|
353 |
|
354 reactions += { |
|
355 case ValueChanged(_) => |
|
356 if (colorator(text)) |
|
357 background = Color.RED |
|
358 else |
|
359 background = Color.WHITE |
|
360 } |
|
361 |
|
362 def getString = text |
|
363 def getBool = true |
|
364 } |
|
365 |
|
366 private class iCheckBox(t: String, s: Boolean) |
|
367 extends CheckBox(t) with Mutator_Input_Value |
|
368 { |
|
369 selected = s |
|
370 |
|
371 def getString = "" |
|
372 def getBool = selected |
|
373 } |
|
374 |
|
375 private object focusTraversal |
|
376 extends FocusTraversalPolicy |
|
377 { |
|
378 private var items = Vector[java.awt.Component]() |
|
379 |
|
380 def add(c: java.awt.Component) { |
|
381 items = items :+ c |
|
382 } |
|
383 def addAll(cs: TraversableOnce[java.awt.Component]) { |
|
384 items = items ++ cs |
|
385 } |
|
386 def clear() { |
|
387 items = Vector[java.awt.Component]() |
|
388 } |
|
389 |
|
390 def getComponentAfter(root: java.awt.Container, |
|
391 c: java.awt.Component): java.awt.Component = { |
|
392 val i = items.indexOf(c) |
|
393 if (i < 0) { |
|
394 getDefaultComponent(root) |
|
395 } else { |
|
396 items((i + 1) % items.length) |
|
397 } |
|
398 } |
|
399 |
|
400 def getComponentBefore(root: java.awt.Container, |
|
401 c: java.awt.Component): java.awt.Component = { |
|
402 val i = items.indexOf(c) |
|
403 if (i < 0) { |
|
404 getDefaultComponent(root) |
|
405 } else { |
|
406 items((i - 1) % items.length) |
|
407 } |
|
408 } |
|
409 |
|
410 def getFirstComponent(root: java.awt.Container): java.awt.Component = { |
|
411 if (items.length > 0) |
|
412 items(0) |
|
413 else |
|
414 null |
|
415 } |
|
416 |
|
417 def getDefaultComponent(root: java.awt.Container) |
|
418 : java.awt.Component = getFirstComponent(root) |
|
419 |
|
420 def getLastComponent(root: java.awt.Container): java.awt.Component = { |
|
421 if (items.length > 0) |
|
422 items.last |
|
423 else |
|
424 null |
|
425 } |
|
426 } |
|
427 } |
|