author | wenzelm |
Thu, 04 Mar 2021 21:04:27 +0100 | |
changeset 73367 | 77ef8bef0593 |
parent 73357 | 31d4274f32de |
child 75393 | 87ebf5a50283 |
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( |
59459 | 23 |
graphview: Graphview, |
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 |
73340 | 34 |
private def panels_=(panels: List[Mutator_Panel]): Unit = |
59218 | 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 |
|
73340 | 46 |
override def open(): Unit = |
59218 | 47 |
{ |
59221 | 48 |
if (!visible) panels = get_panels(container()) |
73367 | 49 |
super.open() |
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 |
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 |
|
73340 | 85 |
private def removePanel(m: Mutator_Panel): Unit = |
59218 | 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 |
|
73340 | 90 |
private def add_panel(m: Mutator_Panel): Unit = |
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 |
|
73340 | 95 |
def paint_panels(): Unit = |
59218 | 96 |
{ |
73367 | 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) |
|
73367 | 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 |
|
71601 | 113 |
val filter_panel: BoxPanel = 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( |
73344 | 120 |
new Mutator_Panel(Mutator.Info(true, graphview.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 { |
73367 | 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 |
|
59391 | 158 |
layout(new ScrollPane(filter_panel)) = BorderPanel.Position.Center |
159 |
layout(botPanel) = BorderPanel.Position.South |
|
49557
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 |
71383 | 182 |
inputs.map({ |
59218 | 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 |
}) |
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 |
val t = this |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
196 |
contents += Swing.HGlue |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
197 |
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
|
198 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
199 |
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
|
200 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
201 |
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
|
202 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
203 |
action = Action("Color") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
204 |
t.background = |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
205 |
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
|
206 |
} |
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 |
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
|
209 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
210 |
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
|
211 |
} |
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 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
214 |
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
|
215 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
216 |
action = Action("Up") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
217 |
movePanelUp(t) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
218 |
} |
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 |
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
|
221 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
222 |
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
|
223 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
224 |
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
|
225 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
226 |
action = Action("Down") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
227 |
movePanelDown(t) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
228 |
} |
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 |
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
|
231 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
232 |
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
|
233 |
contents += new Button { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
234 |
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
|
235 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
236 |
action = Action("Del") { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
237 |
removePanel(t) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
238 |
} |
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 |
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
|
241 |
} |
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 |
focusList = focusList.reverse |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
245 |
|
59221 | 246 |
def get_mutator: Mutator.Info = |
59218 | 247 |
{ |
59459 | 248 |
val model = graphview.model |
59221 | 249 |
val m = |
250 |
initials.mutator match { |
|
251 |
case Mutator.Identity() => |
|
252 |
Mutator.Identity() |
|
253 |
case Mutator.Node_Expression(r, _, _, _) => |
|
59229 | 254 |
val r1 = inputs(2)._2.string |
59221 | 255 |
Mutator.Node_Expression( |
59224 | 256 |
if (Library.make_regex(r1).isDefined) r1 else r, |
59229 | 257 |
inputs(3)._2.bool, |
59221 | 258 |
// "Parents" means "Show parents" or "Matching Children" |
59229 | 259 |
inputs(1)._2.bool, |
260 |
inputs(0)._2.bool) |
|
59221 | 261 |
case Mutator.Node_List(_, _, _, _) => |
262 |
Mutator.Node_List( |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
263 |
for { |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
264 |
ident <- space_explode(',', inputs(2)._2.string) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
265 |
node <- model.find_node(ident) |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
266 |
} yield node, |
59229 | 267 |
inputs(3)._2.bool, |
59221 | 268 |
// "Parents" means "Show parents" or "Matching Children" |
59229 | 269 |
inputs(1)._2.bool, |
270 |
inputs(0)._2.bool) |
|
59246 | 271 |
case Mutator.Edge_Endpoints(_) => |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
272 |
(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
|
273 |
case (Some(node1), Some(node2)) => |
59246 | 274 |
Mutator.Edge_Endpoints((node1, node2)) |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
275 |
case _ => |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
276 |
Mutator.Identity() |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
277 |
} |
59221 | 278 |
case Mutator.Add_Node_Expression(r) => |
59229 | 279 |
val r1 = inputs(0)._2.string |
59224 | 280 |
Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r) |
59221 | 281 |
case Mutator.Add_Transitive_Closure(_, _) => |
282 |
Mutator.Add_Transitive_Closure( |
|
59229 | 283 |
inputs(0)._2.bool, |
284 |
inputs(1)._2.bool) |
|
59221 | 285 |
case _ => |
286 |
Mutator.Identity() |
|
287 |
} |
|
59218 | 288 |
|
59221 | 289 |
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
|
290 |
} |
59218 | 291 |
|
59229 | 292 |
private def get_inputs(): List[(String, Input)] = |
59221 | 293 |
initials.mutator match { |
294 |
case Mutator.Node_Expression(regex, reverse, check_parents, check_children) => |
|
59218 | 295 |
List( |
59229 | 296 |
("", new Check_Box_Input("Parents", check_children)), |
297 |
("", new Check_Box_Input("Children", check_parents)), |
|
298 |
("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)), |
|
299 |
("", new Check_Box_Input(reverse_caption, reverse))) |
|
59221 | 300 |
case Mutator.Node_List(list, reverse, check_parents, check_children) => |
59218 | 301 |
List( |
59229 | 302 |
("", new Check_Box_Input("Parents", check_children)), |
303 |
("", 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
|
304 |
("Names", new Text_Field_Input(list.map(_.ident).mkString(","))), |
59229 | 305 |
("", new Check_Box_Input(reverse_caption, reverse))) |
59246 | 306 |
case Mutator.Edge_Endpoints((source, dest)) => |
59218 | 307 |
List( |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
308 |
("Source", new Text_Field_Input(source.ident)), |
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59240
diff
changeset
|
309 |
("Destination", new Text_Field_Input(dest.ident))) |
59221 | 310 |
case Mutator.Add_Node_Expression(regex) => |
59229 | 311 |
List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined))) |
59221 | 312 |
case Mutator.Add_Transitive_Closure(parents, children) => |
59218 | 313 |
List( |
59229 | 314 |
("", new Check_Box_Input("Parents", parents)), |
315 |
("", new Check_Box_Input("Children", children))) |
|
59218 | 316 |
case _ => Nil |
317 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
318 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
319 |
|
59229 | 320 |
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
|
321 |
{ |
59229 | 322 |
def string: String |
323 |
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
|
324 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
325 |
|
59229 | 326 |
private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true) |
327 |
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
|
328 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
329 |
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
|
330 |
|
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
59224
diff
changeset
|
331 |
private val default_foreground = foreground |
59218 | 332 |
reactions += |
333 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
334 |
case ValueChanged(_) => |
59459 | 335 |
foreground = if (check(text)) default_foreground else graphview.error_color |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
336 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
337 |
|
59229 | 338 |
def string = text |
339 |
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
|
340 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
341 |
|
59229 | 342 |
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
|
343 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
344 |
selected = s |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
345 |
|
59229 | 346 |
def string = "" |
347 |
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
|
348 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
349 |
|
59222 | 350 |
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
|
351 |
{ |
59222 | 352 |
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
|
353 |
|
73340 | 354 |
def add(c: java.awt.Component): Unit = { items = items :+ c } |
73357 | 355 |
def addAll(cs: IterableOnce[java.awt.Component]): Unit = { items = items ++ cs } |
73340 | 356 |
def clear(): Unit = { 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
|
357 |
|
59218 | 358 |
def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component = |
359 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
360 |
val i = items.indexOf(c) |
59218 | 361 |
if (i < 0) getDefaultComponent(root) |
362 |
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
|
363 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
364 |
|
59218 | 365 |
def getComponentBefore(root: java.awt.Container, c: java.awt.Component): java.awt.Component = |
366 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
367 |
val i = items.indexOf(c) |
59218 | 368 |
if (i < 0) getDefaultComponent(root) |
369 |
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
|
370 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
371 |
|
59218 | 372 |
def getFirstComponent(root: java.awt.Container): java.awt.Component = |
71383 | 373 |
if (items.nonEmpty) 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
|
374 |
|
59218 | 375 |
def getDefaultComponent(root: java.awt.Container): java.awt.Component = |
376 |
getFirstComponent(root) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
377 |
|
59218 | 378 |
def getLastComponent(root: java.awt.Container): java.awt.Component = |
71383 | 379 |
if (items.nonEmpty) 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
|
380 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
381 |
} |