author | wenzelm |
Wed, 02 Apr 2014 20:22:12 +0200 | |
changeset 56372 | fadb0fef09d7 |
parent 55618 | 995162143ef4 |
child 58939 | 994fe0ba8335 |
permissions | -rw-r--r-- |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
1 |
/* Title: Tools/Graphview/src/visualizer.scala |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
3 |
|
50475 | 4 |
Graph visualization parameters and interface state. |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
5 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
|
50464 | 9 |
|
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49557
diff
changeset
|
10 |
import isabelle._ |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
|
50476
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
12 |
import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D} |
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
13 |
import java.awt.image.BufferedImage |
49729 | 14 |
import javax.swing.JComponent |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
|
50465 | 17 |
class Visualizer(val model: Model) |
18 |
{ |
|
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
19 |
visualizer => |
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
20 |
|
50476
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
21 |
|
50475 | 22 |
/* font rendering information */ |
23 |
||
24 |
val font_family: String = "IsabelleText" |
|
25 |
val font_size: Int = 14 |
|
50476
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
26 |
val font = new Font(font_family, Font.BOLD, font_size) |
50475 | 27 |
|
28 |
val rendering_hints = |
|
29 |
new RenderingHints( |
|
30 |
RenderingHints.KEY_ANTIALIASING, |
|
31 |
RenderingHints.VALUE_ANTIALIAS_ON) |
|
32 |
||
50476
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
33 |
val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics |
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
34 |
gfx.setFont(font) |
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
35 |
gfx.setRenderingHints(rendering_hints) |
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
36 |
|
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
37 |
val font_metrics: FontMetrics = gfx.getFontMetrics(font) |
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
38 |
|
50475 | 39 |
val tooltip_font_size: Int = 10 |
40 |
||
41 |
||
42 |
/* rendering parameters */ |
|
43 |
||
44 |
val gap_x = 20 |
|
45 |
val pad_x = 8 |
|
46 |
val pad_y = 5 |
|
47 |
||
48 |
var arrow_heads = false |
|
49 |
||
50 |
object Colors |
|
51 |
{ |
|
52 |
private val filter_colors = List( |
|
53 |
new JColor(0xD9, 0xF2, 0xE2), // blue |
|
54 |
new JColor(0xFF, 0xE7, 0xD8), // orange |
|
55 |
new JColor(0xFF, 0xFF, 0xE5), // yellow |
|
56 |
new JColor(0xDE, 0xCE, 0xFF), // lilac |
|
57 |
new JColor(0xCC, 0xEB, 0xFF), // turquoise |
|
58 |
new JColor(0xFF, 0xE5, 0xE5), // red |
|
59 |
new JColor(0xE5, 0xE5, 0xD9) // green |
|
60 |
) |
|
61 |
||
62 |
private var curr : Int = -1 |
|
63 |
def next(): JColor = |
|
64 |
{ |
|
65 |
curr = (curr + 1) % filter_colors.length |
|
66 |
filter_colors(curr) |
|
67 |
} |
|
68 |
} |
|
69 |
||
50472
bad1a1ca61e1
separate instance of class Parameters for each Main_Panel -- avoid global program state;
wenzelm
parents:
50471
diff
changeset
|
70 |
|
50465 | 71 |
object Coordinates |
72 |
{ |
|
50470 | 73 |
private var layout = Layout_Pendulum.empty_layout |
50465 | 74 |
|
75 |
def apply(k: String): (Double, Double) = |
|
50470 | 76 |
layout.nodes.get(k) match { |
50465 | 77 |
case Some(c) => c |
78 |
case None => (0, 0) |
|
79 |
} |
|
80 |
||
81 |
def apply(e: (String, String)): List[(Double, Double)] = |
|
50470 | 82 |
layout.dummies.get(e) match { |
50465 | 83 |
case Some(ds) => ds |
84 |
case None => Nil |
|
85 |
} |
|
86 |
||
87 |
def reposition(k: String, to: (Double, Double)) |
|
88 |
{ |
|
50470 | 89 |
layout = layout.copy(nodes = layout.nodes + (k -> to)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
90 |
} |
50465 | 91 |
|
92 |
def reposition(d: ((String, String), Int), to: (Double, Double)) |
|
93 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
94 |
val (e, index) = d |
50470 | 95 |
layout.dummies.get(e) match { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
96 |
case None => |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
97 |
case Some(ds) => |
50470 | 98 |
layout = layout.copy(dummies = |
99 |
layout.dummies + (e -> |
|
100 |
(ds.zipWithIndex :\ List.empty[(Double, Double)]) { |
|
101 |
case ((t, i), n) => if (index == i) to :: n else t :: n |
|
102 |
})) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
103 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
104 |
} |
50465 | 105 |
|
106 |
def translate(k: String, by: (Double, Double)) |
|
107 |
{ |
|
108 |
val ((x, y), (dx, dy)) = (Coordinates(k), by) |
|
109 |
reposition(k, (x + dx, y + dy)) |
|
110 |
} |
|
111 |
||
112 |
def translate(d: ((String, String), Int), by: (Double, Double)) |
|
113 |
{ |
|
114 |
val ((e, i),(dx, dy)) = (d, by) |
|
115 |
val (x, y) = apply(e)(i) |
|
116 |
reposition(d, (x + dx, y + dy)) |
|
117 |
} |
|
118 |
||
50470 | 119 |
def update_layout() |
50465 | 120 |
{ |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
121 |
layout = |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
122 |
if (model.current.is_empty) Layout_Pendulum.empty_layout |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
123 |
else { |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
124 |
val max_width = |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
55618
diff
changeset
|
125 |
model.current.iterator.map({ case (_, (info, _)) => |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
126 |
font_metrics.stringWidth(info.name).toDouble }).max |
50476
1cb983bccb5b
more official graphics context with font metrics;
wenzelm
parents:
50475
diff
changeset
|
127 |
val box_distance = max_width + pad_x + gap_x |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
128 |
def box_height(n: Int): Double = |
50475 | 129 |
((font_metrics.getAscent + font_metrics.getDescent + pad_y) * (5 max n)).toDouble |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
130 |
Layout_Pendulum(model.current, box_distance, box_height) |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50472
diff
changeset
|
131 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
132 |
} |
50465 | 133 |
|
134 |
def bounds(): (Double, Double, Double, Double) = |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
55618
diff
changeset
|
135 |
model.visible_nodes_iterator.toList match { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
136 |
case Nil => (0, 0, 0, 0) |
50465 | 137 |
case nodes => |
138 |
val X: (String => Double) = (n => apply(n)._1) |
|
139 |
val Y: (String => Double) = (n => apply(n)._2) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
140 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
141 |
(X(nodes.minBy(X)), Y(nodes.minBy(Y)), |
50465 | 142 |
X(nodes.maxBy(X)), Y(nodes.maxBy(Y))) |
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 |
} |
50465 | 145 |
|
50464 | 146 |
object Drawer |
147 |
{ |
|
50465 | 148 |
def apply(g: Graphics2D, n: Option[String]) |
149 |
{ |
|
150 |
n match { |
|
151 |
case None => |
|
152 |
case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n) |
|
153 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
154 |
} |
50465 | 155 |
|
156 |
def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean) |
|
157 |
{ |
|
158 |
Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
159 |
} |
50465 | 160 |
|
50464 | 161 |
def paint_all_visible(g: Graphics2D, dummies: Boolean) |
162 |
{ |
|
50465 | 163 |
g.setFont(font) |
50464 | 164 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
165 |
g.setRenderingHints(rendering_hints) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
166 |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
55618
diff
changeset
|
167 |
model.visible_edges_iterator.foreach(e => { |
50475 | 168 |
apply(g, e, arrow_heads, dummies) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
169 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
170 |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
55618
diff
changeset
|
171 |
model.visible_nodes_iterator.foreach(l => { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
172 |
apply(g, Some(l)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
173 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
174 |
} |
50465 | 175 |
|
176 |
def shape(g: Graphics2D, n: Option[String]): Shape = |
|
177 |
n match { |
|
178 |
case None => Shapes.Dummy.shape(g, visualizer, None) |
|
179 |
case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n) |
|
180 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
181 |
} |
50465 | 182 |
|
183 |
object Selection |
|
184 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
185 |
private var selected: List[String] = Nil |
50465 | 186 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
187 |
def apply() = selected |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
188 |
def apply(s: String) = selected.contains(s) |
50465 | 189 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
190 |
def add(s: String) { selected = s :: selected } |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
191 |
def set(ss: List[String]) { selected = ss } |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
192 |
def clear() { selected = Nil } |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
193 |
} |
50465 | 194 |
|
50464 | 195 |
object Color |
196 |
{ |
|
50465 | 197 |
def apply(l: Option[String]): (JColor, JColor, JColor) = |
198 |
l match { |
|
199 |
case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK) |
|
200 |
case Some(c) => { |
|
201 |
if (Selection(c)) |
|
202 |
(JColor.BLUE, JColor.GREEN, JColor.BLACK) |
|
203 |
else |
|
204 |
(JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK) |
|
205 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
206 |
} |
50464 | 207 |
|
50465 | 208 |
def apply(e: (String, String)): JColor = JColor.BLACK |
209 |
} |
|
210 |
||
211 |
object Caption |
|
50464 | 212 |
{ |
50471
a5930c929b1e
discontinued long names flag -- better done via entity markup, without affecting layout;
wenzelm
parents:
50470
diff
changeset
|
213 |
def apply(key: String) = model.complete.get_node(key).name |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
214 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
215 |
} |