1 /* Title: Tools/Graphview/src/visualizer.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Graph visualization parameters and interface state. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D} |
|
13 import java.awt.image.BufferedImage |
|
14 import javax.swing.JComponent |
|
15 |
|
16 |
|
17 class Visualizer(val model: Model) |
|
18 { |
|
19 visualizer => |
|
20 |
|
21 |
|
22 /* font rendering information */ |
|
23 |
|
24 val font_family: String = "IsabelleText" |
|
25 val font_size: Int = 14 |
|
26 val font = new Font(font_family, Font.BOLD, font_size) |
|
27 |
|
28 val rendering_hints = |
|
29 new RenderingHints( |
|
30 RenderingHints.KEY_ANTIALIASING, |
|
31 RenderingHints.VALUE_ANTIALIAS_ON) |
|
32 |
|
33 val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics |
|
34 gfx.setFont(font) |
|
35 gfx.setRenderingHints(rendering_hints) |
|
36 |
|
37 val font_metrics: FontMetrics = gfx.getFontMetrics(font) |
|
38 |
|
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 |
|
70 |
|
71 object Coordinates |
|
72 { |
|
73 private var layout = Layout_Pendulum.empty_layout |
|
74 |
|
75 def apply(k: String): (Double, Double) = |
|
76 layout.nodes.get(k) match { |
|
77 case Some(c) => c |
|
78 case None => (0, 0) |
|
79 } |
|
80 |
|
81 def apply(e: (String, String)): List[(Double, Double)] = |
|
82 layout.dummies.get(e) match { |
|
83 case Some(ds) => ds |
|
84 case None => Nil |
|
85 } |
|
86 |
|
87 def reposition(k: String, to: (Double, Double)) |
|
88 { |
|
89 layout = layout.copy(nodes = layout.nodes + (k -> to)) |
|
90 } |
|
91 |
|
92 def reposition(d: ((String, String), Int), to: (Double, Double)) |
|
93 { |
|
94 val (e, index) = d |
|
95 layout.dummies.get(e) match { |
|
96 case None => |
|
97 case Some(ds) => |
|
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 })) |
|
103 } |
|
104 } |
|
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 |
|
119 def update_layout() |
|
120 { |
|
121 layout = |
|
122 if (model.current.is_empty) Layout_Pendulum.empty_layout |
|
123 else { |
|
124 val max_width = |
|
125 model.current.iterator.map({ case (_, (info, _)) => |
|
126 font_metrics.stringWidth(info.name).toDouble }).max |
|
127 val box_distance = max_width + pad_x + gap_x |
|
128 def box_height(n: Int): Double = |
|
129 ((font_metrics.getAscent + font_metrics.getDescent + pad_y) * (5 max n)).toDouble |
|
130 Layout_Pendulum(model.current, box_distance, box_height) |
|
131 } |
|
132 } |
|
133 |
|
134 def bounds(): (Double, Double, Double, Double) = |
|
135 model.visible_nodes_iterator.toList match { |
|
136 case Nil => (0, 0, 0, 0) |
|
137 case nodes => |
|
138 val X: (String => Double) = (n => apply(n)._1) |
|
139 val Y: (String => Double) = (n => apply(n)._2) |
|
140 |
|
141 (X(nodes.minBy(X)), Y(nodes.minBy(Y)), |
|
142 X(nodes.maxBy(X)), Y(nodes.maxBy(Y))) |
|
143 } |
|
144 } |
|
145 |
|
146 object Drawer |
|
147 { |
|
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 } |
|
154 } |
|
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) |
|
159 } |
|
160 |
|
161 def paint_all_visible(g: Graphics2D, dummies: Boolean) |
|
162 { |
|
163 g.setFont(font) |
|
164 |
|
165 g.setRenderingHints(rendering_hints) |
|
166 |
|
167 model.visible_edges_iterator.foreach(e => { |
|
168 apply(g, e, arrow_heads, dummies) |
|
169 }) |
|
170 |
|
171 model.visible_nodes_iterator.foreach(l => { |
|
172 apply(g, Some(l)) |
|
173 }) |
|
174 } |
|
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 } |
|
181 } |
|
182 |
|
183 object Selection |
|
184 { |
|
185 private var selected: List[String] = Nil |
|
186 |
|
187 def apply() = selected |
|
188 def apply(s: String) = selected.contains(s) |
|
189 |
|
190 def add(s: String) { selected = s :: selected } |
|
191 def set(ss: List[String]) { selected = ss } |
|
192 def clear() { selected = Nil } |
|
193 } |
|
194 |
|
195 object Color |
|
196 { |
|
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 } |
|
206 } |
|
207 |
|
208 def apply(e: (String, String)): JColor = JColor.BLACK |
|
209 } |
|
210 |
|
211 object Caption |
|
212 { |
|
213 def apply(key: String) = model.complete.get_node(key).name |
|
214 } |
|
215 } |
|