--- a/src/Tools/Graphview/src/visualizer.scala Mon Dec 10 17:44:17 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala Mon Dec 10 19:17:16 2012 +0100
@@ -10,91 +10,100 @@
import isabelle._
-import java.awt.{Font => JFont, Color => JColor, Shape}
+import java.awt.{Font, Color => JColor, Shape}
import java.awt.{RenderingHints, Graphics2D}
import javax.swing.JComponent
-class Visualizer(val model: Model) {
- object Coordinates {
- private var nodes = Map[String, (Double, Double)]()
- private var dummies = Map[(String, String), List[(Double, Double)]]()
-
- def apply(k: String): (Double, Double) = nodes.get(k) match {
- case Some(c) => c
- case None => (0, 0)
- }
-
- def apply(e: (String, String)): List[(Double, Double)] = dummies.get(e) match {
- case Some(ds) => ds
- case None => Nil
- }
-
- def translate(k: String, by: (Double, Double)) {
- val ((x, y), (dx, dy)) = (Coordinates(k), by)
- reposition(k, (x + dx, y + dy))
- }
-
- def reposition(k: String, to: (Double, Double)) {
+class Visualizer(val model: Model)
+{
+ object Coordinates
+ {
+ private var nodes = Map.empty[String, (Double, Double)]
+ private var dummies = Map.empty[(String, String), List[(Double, Double)]]
+
+ def apply(k: String): (Double, Double) =
+ nodes.get(k) match {
+ case Some(c) => c
+ case None => (0, 0)
+ }
+
+ def apply(e: (String, String)): List[(Double, Double)] =
+ dummies.get(e) match {
+ case Some(ds) => ds
+ case None => Nil
+ }
+
+ def reposition(k: String, to: (Double, Double))
+ {
nodes += (k -> to)
}
-
- def translate(d: ((String, String), Int), by: (Double, Double)) {
- val ((e, i),(dx, dy)) = (d, by)
- val (x, y) = apply(e)(i)
- reposition(d, (x + dx, y + dy))
- }
-
- def reposition(d: ((String, String), Int), to: (Double, Double)) {
+
+ def reposition(d: ((String, String), Int), to: (Double, Double))
+ {
val (e, index) = d
dummies.get(e) match {
case None =>
case Some(ds) =>
- dummies += ( e ->
- (ds.zipWithIndex :\ List[(Double, Double)]()){
- case ((t, i), n) => if (index == i) to :: n
- else t :: n
+ dummies += (e ->
+ (ds.zipWithIndex :\ List[(Double, Double)]()) {
+ case ((t, i), n) => if (index == i) to :: n else t :: n
}
)
}
}
-
- def layout() {
+
+ def translate(k: String, by: (Double, Double))
+ {
+ val ((x, y), (dx, dy)) = (Coordinates(k), by)
+ reposition(k, (x + dx, y + dy))
+ }
+
+ def translate(d: ((String, String), Int), by: (Double, Double))
+ {
+ val ((e, i),(dx, dy)) = (d, by)
+ val (x, y) = apply(e)(i)
+ reposition(d, (x + dx, y + dy))
+ }
+
+ def layout()
+ {
val (l, d) = Layout_Pendulum(model.current)
nodes = l
dummies = d
}
-
- def bounds(): (Double, Double, Double, Double) =
+
+ def bounds(): (Double, Double, Double, Double) =
model.visible_nodes().toList match {
case Nil => (0, 0, 0, 0)
- case nodes => {
- val X: (String => Double) = {n => apply(n)._1}
- val Y: (String => Double) = {n => apply(n)._2}
+ case nodes =>
+ val X: (String => Double) = (n => apply(n)._1)
+ val Y: (String => Double) = (n => apply(n)._2)
(X(nodes.minBy(X)), Y(nodes.minBy(Y)),
- X(nodes.maxBy(X)), Y(nodes.maxBy(Y)))
- }
+ X(nodes.maxBy(X)), Y(nodes.maxBy(Y)))
}
}
-
+
private val visualizer = this
object Drawer
{
- import Shapes._
-
- def apply(g: Graphics2D, n: Option[String]) = n match {
- case None =>
- case Some(_) => Growing_Node.paint(g, visualizer, n)
+ def apply(g: Graphics2D, n: Option[String])
+ {
+ n match {
+ case None =>
+ case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n)
+ }
}
-
- def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean) = {
- Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
+
+ def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean)
+ {
+ Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
}
-
+
def paint_all_visible(g: Graphics2D, dummies: Boolean)
{
- g.setFont(Font())
+ g.setFont(font)
g.setRenderingHints(rendering_hints)
@@ -106,52 +115,51 @@
apply(g, Some(l))
})
}
-
- def shape(g: Graphics2D, n: Option[String]): Shape = n match {
- case None => Dummy.shape(g, visualizer, None)
- case Some(_) => Growing_Node.shape(g, visualizer, n)
- }
+
+ def shape(g: Graphics2D, n: Option[String]): Shape =
+ n match {
+ case None => Shapes.Dummy.shape(g, visualizer, None)
+ case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n)
+ }
}
-
- object Selection {
+
+ object Selection
+ {
private var selected: List[String] = Nil
-
+
def apply() = selected
def apply(s: String) = selected.contains(s)
-
+
def add(s: String) { selected = s :: selected }
def set(ss: List[String]) { selected = ss }
def clear() { selected = Nil }
}
-
+
object Color
{
- def apply(l: Option[String]): (JColor, JColor, JColor) = l match {
- case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK)
- case Some(c) => {
- if (Selection(c))
- (JColor.BLUE, JColor.GREEN, JColor.BLACK)
- else
- (JColor.BLACK,
- model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK)
+ def apply(l: Option[String]): (JColor, JColor, JColor) =
+ l match {
+ case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK)
+ case Some(c) => {
+ if (Selection(c))
+ (JColor.BLUE, JColor.GREEN, JColor.BLACK)
+ else
+ (JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK)
+ }
}
- }
-
- def apply(e: (String, String)): JColor = JColor.BLACK
- }
- object Font
+ def apply(e: (String, String)): JColor = JColor.BLACK
+ }
+
+ object Caption
{
- def apply(): JFont =
- new JFont(Parameters.font_family, JFont.BOLD, Parameters.font_size)
- }
-
- object Caption {
def apply(key: String) =
if (Parameters.long_names) key
else model.complete.get_node(key).name
}
+ val font = new Font(Parameters.font_family, Font.BOLD, Parameters.font_size)
+
val rendering_hints =
new RenderingHints(
RenderingHints.KEY_ANTIALIASING,