author | wenzelm |
Sat, 03 Jan 2015 20:28:53 +0100 | |
changeset 59246 | 32903b99c2ef |
parent 59245 | be4180f3c236 |
child 59391 | 39a38657d16b |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/mutator_dialog.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 |
Mutator selection and configuration dialog. |
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 |
|
55618 | 10 |
|
49558 | 11 |
import isabelle._ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
12 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
13 |
import java.awt.Color |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
14 |
import java.awt.FocusTraversalPolicy |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
import javax.swing.JColorChooser |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
import javax.swing.border.EmptyBorder |
59222 | 17 |
import scala.swing.{Dialog, Button, BoxPanel, Swing, Orientation, ComboBox, Action, |
18 |
Dimension, BorderPanel, ScrollPane, Label, CheckBox, Alignment, Component, TextField} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
19 |
import scala.swing.event.ValueChanged |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
20 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
21 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
22 |
class Mutator_Dialog( |
50475 | 23 |
visualizer: Visualizer, |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50467
diff
changeset
|
24 |
container: Mutator_Container, |
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50467
diff
changeset
|
25 |
caption: String, |
49733
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
26 |
reverse_caption: String = "Inverse", |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
27 |
show_color_chooser: Boolean = true) |
38a68e6593be
prefer synchronous Mutator_Event.Bus on Swing_Thread;
wenzelm
parents:
49565
diff
changeset
|
28 |
extends Dialog |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
29 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
30 |
title = caption |
59218 | 31 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
32 |
private var _panels: List[Mutator_Panel] = Nil |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
33 |
private def panels = _panels |
59218 | 34 |
private def panels_=(panels: List[Mutator_Panel]) |
35 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
36 |
_panels = panels |
59222 | 37 |
paint_panels() |
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 |
container.events += |
41 |
{ |
|
59222 | 42 |
case Mutator_Event.Add(m) => add_panel(new Mutator_Panel(m)) |
59221 | 43 |
case Mutator_Event.New_List(ms) => panels = get_panels(ms) |
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 |
override def open() |
47 |
{ |
|
59221 | 48 |
if (!visible) panels = get_panels(container()) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
49 |
super.open |
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 |
minimumSize = new Dimension(700, 200) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
53 |
preferredSize = new Dimension(1000, 300) |
59222 | 54 |
peer.setFocusTraversalPolicy(Focus_Traveral_Policy) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
55 |
|
59221 | 56 |
private def get_panels(m: List[Mutator.Info]): List[Mutator_Panel] = |
57 |
m.filter({ case Mutator.Info(_, _, Mutator.Identity()) => false case _ => true }) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
58 |
.map(m => new Mutator_Panel(m)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
59 |
|
59221 | 60 |
private def get_mutators(panels: List[Mutator_Panel]): List[Mutator.Info] = |
61 |
panels.map(panel => panel.get_mutator) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
62 |
|
59218 | 63 |
private def movePanelUp(m: Mutator_Panel) = |
64 |
{ |
|
65 |
def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = |
|
66 |
l match { |
|
67 |
case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs) |
|
68 |
case _ => l |
|
69 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
70 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
71 |
panels = moveUp(panels) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
72 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
73 |
|
59218 | 74 |
private def movePanelDown(m: Mutator_Panel) = |
75 |
{ |
|
76 |
def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = |
|
77 |
l match { |
|
78 |
case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs) |
|
79 |
case _ => l |
|
80 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
81 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
82 |
panels = moveDown(panels) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
83 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
84 |
|
59218 | 85 |
private def removePanel(m: Mutator_Panel) |
86 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
87 |
panels = panels.filter(_ != m).toList |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
88 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
89 |
|
59222 | 90 |
private def add_panel(m: Mutator_Panel) |
59218 | 91 |
{ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
92 |
panels = panels ::: List(m) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
93 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
94 |
|
59222 | 95 |
def paint_panels() |
59218 | 96 |
{ |
59222 | 97 |
Focus_Traveral_Policy.clear |
98 |
filter_panel.contents.clear |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
99 |
panels.map(x => { |
59222 | 100 |
filter_panel.contents += x |
101 |
Focus_Traveral_Policy.addAll(x.focusList) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
102 |
}) |
59222 | 103 |
filter_panel.contents += Swing.VGlue |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
104 |
|
59222 | 105 |
Focus_Traveral_Policy.add(mutator_box.peer.asInstanceOf[java.awt.Component]) |
106 |
Focus_Traveral_Policy.add(add_button.peer) |
|
107 |
Focus_Traveral_Policy.add(apply_button.peer) |
|
108 |
Focus_Traveral_Policy.add(cancel_button.peer) |
|
109 |
filter_panel.revalidate |
|
110 |
filter_panel.repaint |
|
49557
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 |
|
59222 | 113 |
val filter_panel = new BoxPanel(Orientation.Vertical) {} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
114 |
|
59221 | 115 |
private val mutator_box = new ComboBox[Mutator](container.available) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
116 |
|
59222 | 117 |
private val add_button = new Button { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
118 |
action = Action("Add") { |
59222 | 119 |
add_panel( |
59221 | 120 |
new Mutator_Panel(Mutator.Info(true, visualizer.Colors.next, mutator_box.selection.item))) |
49557
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 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
123 |
|
59221 | 124 |
private val apply_button = new Button { |
125 |
action = Action("Apply") { container(get_mutators(panels)) } |
|
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 |
|
59221 | 128 |
private val reset_button = new Button { |
129 |
action = Action("Reset") { panels = get_panels(container()) } |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
130 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
131 |
|
59221 | 132 |
private val cancel_button = new Button { |
133 |
action = Action("Close") { close } |
|
59218 | 134 |
} |
59221 | 135 |
defaultButton = cancel_button |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
136 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
137 |
private val botPanel = new BoxPanel(Orientation.Horizontal) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
138 |
border = new EmptyBorder(10, 0, 0, 0) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
139 |
|
59221 | 140 |
contents += mutator_box |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
141 |
contents += Swing.RigidBox(new Dimension(10, 0)) |
59221 | 142 |
contents += add_button |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
143 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
144 |
contents += Swing.HGlue |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
145 |
contents += Swing.RigidBox(new Dimension(30, 0)) |
59221 | 146 |
contents += apply_button |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
147 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
148 |
contents += Swing.RigidBox(new Dimension(5, 0)) |
59221 | 149 |
contents += reset_button |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
150 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
151 |
contents += Swing.RigidBox(new Dimension(5, 0)) |
59221 | 152 |
contents += cancel_button |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
153 |
} |
59218 | 154 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
155 |
contents = new BorderPanel { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
156 |
border = new EmptyBorder(5, 5, 5, 5) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
157 |
|
59222 | 158 |
add(new ScrollPane(filter_panel), BorderPanel.Position.Center) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
159 |
add(botPanel, BorderPanel.Position.South) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
160 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
|
59221 | 162 |
private class Mutator_Panel(initials: Mutator.Info) |
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50467
diff
changeset
|
163 |
extends BoxPanel(Orientation.Horizontal) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
164 |
{ |
59229 | 165 |
private val inputs: List[(String, Input)] = get_inputs() |
50467 | 166 |
var focusList = List.empty[java.awt.Component] |
59229 | 167 |
private val enabledBox = new Check_Box_Input("Enabled", initials.enabled) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
168 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
169 |
border = new EmptyBorder(5, 5, 5, 5) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
170 |
maximumSize = new Dimension(Integer.MAX_VALUE, 30) |
59221 | 171 |
background = initials.color |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
172 |
|
59221 | 173 |
contents += new Label(initials.mutator.name) { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
174 |
preferredSize = new Dimension(175, 20) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
175 |
horizontalAlignment = Alignment.Left |
59221 | 176 |
if (initials.mutator.description != "") tooltip = initials.mutator.description |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
177 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
178 |
contents += Swing.RigidBox(new Dimension(10, 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
179 |
contents += enabledBox |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
180 |
contents += Swing.RigidBox(new Dimension(5, 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
181 |
focusList = enabledBox.peer :: focusList |
59218 | 182 |
inputs.map(_ match { |
183 |
case (n, c) => |
|
184 |
contents += Swing.RigidBox(new Dimension(10, 0)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
185 |
if (n != "") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
186 |
contents += new Label(n) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
187 |
contents += Swing.RigidBox(new Dimension(5, 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
188 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
189 |
contents += c.asInstanceOf[Component] |
59218 | 190 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
191 |
focusList = c.asInstanceOf[Component].peer :: focusList |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
192 |
case _ => |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
193 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
194 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
195 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
196 |
val t = this |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
197 |
contents += Swing.HGlue |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
198 |
contents += Swing.RigidBox(new Dimension(10, 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
199 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
200 |
if (show_color_chooser) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
201 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
202 |
maximumSize = new Dimension(20, 20) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
203 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
204 |
action = Action("Color") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
205 |
t.background = |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
206 |
JColorChooser.showDialog(t.peer, "Choose new Color", t.background) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
207 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
208 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
209 |
focusList = this.peer :: focusList |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
210 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
211 |
contents += Swing.RigidBox(new Dimension(2, 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
212 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
213 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
214 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
215 |
maximumSize = new Dimension(20, 20) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
216 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
217 |
action = Action("Up") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
218 |
movePanelUp(t) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
219 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
220 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
221 |
focusList = this.peer :: focusList |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
222 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
223 |
contents += Swing.RigidBox(new Dimension(2, 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
224 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
225 |
maximumSize = new Dimension(20, 20) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
226 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
227 |
action = Action("Down") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
228 |
movePanelDown(t) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
229 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
230 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
231 |
focusList = this.peer :: focusList |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
232 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
233 |
contents += Swing.RigidBox(new Dimension(2, 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
234 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
235 |
maximumSize = new Dimension(20, 20) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
236 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
237 |
action = Action("Del") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
238 |
removePanel(t) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
239 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
240 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
241 |
focusList = this.peer :: focusList |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
242 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
243 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
244 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
245 |
focusList = focusList.reverse |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
246 |
|
59221 | 247 |
def get_mutator: Mutator.Info = |
59218 | 248 |
{ |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
249 |
val model = visualizer.model |
59221 | 250 |
val m = |
251 |
initials.mutator match { |
|
252 |
case Mutator.Identity() => |
|
253 |
Mutator.Identity() |
|
254 |
case Mutator.Node_Expression(r, _, _, _) => |
|
59229 | 255 |
val r1 = inputs(2)._2.string |
59221 | 256 |
Mutator.Node_Expression( |
59224 | 257 |
if (Library.make_regex(r1).isDefined) r1 else r, |
59229 | 258 |
inputs(3)._2.bool, |
59221 | 259 |
// "Parents" means "Show parents" or "Matching Children" |
59229 | 260 |
inputs(1)._2.bool, |
261 |
inputs(0)._2.bool) |
|
59221 | 262 |
case Mutator.Node_List(_, _, _, _) => |
263 |
Mutator.Node_List( |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
264 |
for { |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
265 |
ident <- space_explode(',', inputs(2)._2.string) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
266 |
node <- model.find_node(ident) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
267 |
} yield node, |
59229 | 268 |
inputs(3)._2.bool, |
59221 | 269 |
// "Parents" means "Show parents" or "Matching Children" |
59229 | 270 |
inputs(1)._2.bool, |
271 |
inputs(0)._2.bool) |
|
59246 | 272 |
case Mutator.Edge_Endpoints(_) => |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
273 |
(model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match { |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
274 |
case (Some(node1), Some(node2)) => |
59246 | 275 |
Mutator.Edge_Endpoints((node1, node2)) |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
276 |
case _ => |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
277 |
Mutator.Identity() |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
278 |
} |
59221 | 279 |
case Mutator.Add_Node_Expression(r) => |
59229 | 280 |
val r1 = inputs(0)._2.string |
59224 | 281 |
Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r) |
59221 | 282 |
case Mutator.Add_Transitive_Closure(_, _) => |
283 |
Mutator.Add_Transitive_Closure( |
|
59229 | 284 |
inputs(0)._2.bool, |
285 |
inputs(1)._2.bool) |
|
59221 | 286 |
case _ => |
287 |
Mutator.Identity() |
|
288 |
} |
|
59218 | 289 |
|
59221 | 290 |
Mutator.Info(enabledBox.selected, background, m) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
291 |
} |
59218 | 292 |
|
59229 | 293 |
private def get_inputs(): List[(String, Input)] = |
59221 | 294 |
initials.mutator match { |
295 |
case Mutator.Node_Expression(regex, reverse, check_parents, check_children) => |
|
59218 | 296 |
List( |
59229 | 297 |
("", new Check_Box_Input("Parents", check_children)), |
298 |
("", new Check_Box_Input("Children", check_parents)), |
|
299 |
("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)), |
|
300 |
("", new Check_Box_Input(reverse_caption, reverse))) |
|
59221 | 301 |
case Mutator.Node_List(list, reverse, check_parents, check_children) => |
59218 | 302 |
List( |
59229 | 303 |
("", new Check_Box_Input("Parents", check_children)), |
304 |
("", new Check_Box_Input("Children", check_parents)), |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
305 |
("Names", new Text_Field_Input(list.map(_.ident).mkString(","))), |
59229 | 306 |
("", new Check_Box_Input(reverse_caption, reverse))) |
59246 | 307 |
case Mutator.Edge_Endpoints((source, dest)) => |
59218 | 308 |
List( |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
309 |
("Source", new Text_Field_Input(source.ident)), |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
310 |
("Destination", new Text_Field_Input(dest.ident))) |
59221 | 311 |
case Mutator.Add_Node_Expression(regex) => |
59229 | 312 |
List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined))) |
59221 | 313 |
case Mutator.Add_Transitive_Closure(parents, children) => |
59218 | 314 |
List( |
59229 | 315 |
("", new Check_Box_Input("Parents", parents)), |
316 |
("", new Check_Box_Input("Children", children))) |
|
59218 | 317 |
case _ => Nil |
318 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
319 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
320 |
|
59229 | 321 |
private trait Input |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
322 |
{ |
59229 | 323 |
def string: String |
324 |
def bool: Boolean |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
325 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
326 |
|
59229 | 327 |
private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true) |
328 |
extends TextField(txt) with Input |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
329 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
330 |
preferredSize = new Dimension(125, 18) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
331 |
|
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59224
diff
changeset
|
332 |
private val default_foreground = foreground |
59218 | 333 |
reactions += |
334 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
335 |
case ValueChanged(_) => |
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59224
diff
changeset
|
336 |
foreground = if (check(text)) default_foreground else visualizer.error_color |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
337 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
338 |
|
59229 | 339 |
def string = text |
340 |
def bool = true |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
341 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
342 |
|
59229 | 343 |
private class Check_Box_Input(txt: String, s: Boolean) extends CheckBox(txt) with Input |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
344 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
345 |
selected = s |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
346 |
|
59229 | 347 |
def string = "" |
348 |
def bool = selected |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
349 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
350 |
|
59222 | 351 |
private object Focus_Traveral_Policy extends FocusTraversalPolicy |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
352 |
{ |
59222 | 353 |
private var items = Vector.empty[java.awt.Component] |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
354 |
|
59218 | 355 |
def add(c: java.awt.Component) { items = items :+ c } |
356 |
def addAll(cs: TraversableOnce[java.awt.Component]) { items = items ++ cs } |
|
59222 | 357 |
def clear() { items = Vector.empty } |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
358 |
|
59218 | 359 |
def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component = |
360 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
361 |
val i = items.indexOf(c) |
59218 | 362 |
if (i < 0) getDefaultComponent(root) |
363 |
else items((i + 1) % items.length) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
364 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
365 |
|
59218 | 366 |
def getComponentBefore(root: java.awt.Container, c: java.awt.Component): java.awt.Component = |
367 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
368 |
val i = items.indexOf(c) |
59218 | 369 |
if (i < 0) getDefaultComponent(root) |
370 |
else items((i - 1) % items.length) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
371 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
372 |
|
59218 | 373 |
def getFirstComponent(root: java.awt.Container): java.awt.Component = |
374 |
if (items.length > 0) items(0) else null |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
375 |
|
59218 | 376 |
def getDefaultComponent(root: java.awt.Container): java.awt.Component = |
377 |
getFirstComponent(root) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
378 |
|
59218 | 379 |
def getLastComponent(root: java.awt.Container): java.awt.Component = |
380 |
if (items.length > 0) items.last else null |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
381 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
382 |
} |