author | wenzelm |
Mon, 10 Dec 2012 19:42:58 +0100 | |
changeset 50467 | 4b0e69dc9db8 |
parent 50465 | 0afb01666df2 |
child 50470 | cb73e91bb019 |
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 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
Graph visualization interface. |
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 |
|
50464 | 12 |
|
50465 | 13 |
import java.awt.{Font, Color => JColor, Shape} |
49557
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.{RenderingHints, Graphics2D} |
49729 | 15 |
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
|
16 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
|
50465 | 18 |
class Visualizer(val model: Model) |
19 |
{ |
|
20 |
object Coordinates |
|
21 |
{ |
|
22 |
private var nodes = Map.empty[String, (Double, Double)] |
|
23 |
private var dummies = Map.empty[(String, String), List[(Double, Double)]] |
|
24 |
||
25 |
def apply(k: String): (Double, Double) = |
|
26 |
nodes.get(k) match { |
|
27 |
case Some(c) => c |
|
28 |
case None => (0, 0) |
|
29 |
} |
|
30 |
||
31 |
def apply(e: (String, String)): List[(Double, Double)] = |
|
32 |
dummies.get(e) match { |
|
33 |
case Some(ds) => ds |
|
34 |
case None => Nil |
|
35 |
} |
|
36 |
||
37 |
def reposition(k: String, to: (Double, Double)) |
|
38 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
39 |
nodes += (k -> to) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
40 |
} |
50465 | 41 |
|
42 |
def reposition(d: ((String, String), Int), to: (Double, Double)) |
|
43 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
44 |
val (e, index) = d |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
45 |
dummies.get(e) match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
46 |
case None => |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
47 |
case Some(ds) => |
50465 | 48 |
dummies += (e -> |
50467 | 49 |
(ds.zipWithIndex :\ List.empty[(Double, Double)]) { |
50465 | 50 |
case ((t, i), n) => if (index == i) to :: n else t :: n |
49557
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 |
) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
53 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
54 |
} |
50465 | 55 |
|
56 |
def translate(k: String, by: (Double, Double)) |
|
57 |
{ |
|
58 |
val ((x, y), (dx, dy)) = (Coordinates(k), by) |
|
59 |
reposition(k, (x + dx, y + dy)) |
|
60 |
} |
|
61 |
||
62 |
def translate(d: ((String, String), Int), by: (Double, Double)) |
|
63 |
{ |
|
64 |
val ((e, i),(dx, dy)) = (d, by) |
|
65 |
val (x, y) = apply(e)(i) |
|
66 |
reposition(d, (x + dx, y + dy)) |
|
67 |
} |
|
68 |
||
69 |
def layout() |
|
70 |
{ |
|
50467 | 71 |
val (l, d) = Layout_Pendulum(model.current) // FIXME avoid computation on Swing thread |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
72 |
nodes = l |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
73 |
dummies = d |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
74 |
} |
50465 | 75 |
|
76 |
def bounds(): (Double, Double, Double, Double) = |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
77 |
model.visible_nodes().toList match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
78 |
case Nil => (0, 0, 0, 0) |
50465 | 79 |
case nodes => |
80 |
val X: (String => Double) = (n => apply(n)._1) |
|
81 |
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
|
82 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
83 |
(X(nodes.minBy(X)), Y(nodes.minBy(Y)), |
50465 | 84 |
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
|
85 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
86 |
} |
50465 | 87 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
88 |
private val visualizer = this |
50464 | 89 |
object Drawer |
90 |
{ |
|
50465 | 91 |
def apply(g: Graphics2D, n: Option[String]) |
92 |
{ |
|
93 |
n match { |
|
94 |
case None => |
|
95 |
case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n) |
|
96 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
97 |
} |
50465 | 98 |
|
99 |
def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean) |
|
100 |
{ |
|
101 |
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
|
102 |
} |
50465 | 103 |
|
50464 | 104 |
def paint_all_visible(g: Graphics2D, dummies: Boolean) |
105 |
{ |
|
50465 | 106 |
g.setFont(font) |
50464 | 107 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
108 |
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
|
109 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
110 |
model.visible_edges().foreach(e => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
111 |
apply(g, e, Parameters.arrow_heads, dummies) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
112 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
113 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
114 |
model.visible_nodes().foreach(l => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
115 |
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
|
116 |
}) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
117 |
} |
50465 | 118 |
|
119 |
def shape(g: Graphics2D, n: Option[String]): Shape = |
|
120 |
n match { |
|
121 |
case None => Shapes.Dummy.shape(g, visualizer, None) |
|
122 |
case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n) |
|
123 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
124 |
} |
50465 | 125 |
|
126 |
object Selection |
|
127 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
128 |
private var selected: List[String] = Nil |
50465 | 129 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
130 |
def apply() = selected |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
131 |
def apply(s: String) = selected.contains(s) |
50465 | 132 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
133 |
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
|
134 |
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
|
135 |
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
|
136 |
} |
50465 | 137 |
|
50464 | 138 |
object Color |
139 |
{ |
|
50465 | 140 |
def apply(l: Option[String]): (JColor, JColor, JColor) = |
141 |
l match { |
|
142 |
case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK) |
|
143 |
case Some(c) => { |
|
144 |
if (Selection(c)) |
|
145 |
(JColor.BLUE, JColor.GREEN, JColor.BLACK) |
|
146 |
else |
|
147 |
(JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK) |
|
148 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
149 |
} |
50464 | 150 |
|
50465 | 151 |
def apply(e: (String, String)): JColor = JColor.BLACK |
152 |
} |
|
153 |
||
154 |
object Caption |
|
50464 | 155 |
{ |
49736
dfa100466d2e
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
wenzelm
parents:
49732
diff
changeset
|
156 |
def apply(key: String) = |
dfa100466d2e
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
wenzelm
parents:
49732
diff
changeset
|
157 |
if (Parameters.long_names) key |
dfa100466d2e
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
wenzelm
parents:
49732
diff
changeset
|
158 |
else 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
|
159 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
160 |
|
50465 | 161 |
val font = new Font(Parameters.font_family, Font.BOLD, Parameters.font_size) |
162 |
||
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
163 |
val rendering_hints = |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
164 |
new RenderingHints( |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
165 |
RenderingHints.KEY_ANTIALIASING, |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
166 |
RenderingHints.VALUE_ANTIALIAS_ON) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
167 |
} |