# HG changeset patch # User wenzelm # Date 1355163436 -3600 # Node ID 0afb01666df2ef550455da5863ca141003ba3c89 # Parent 37b53813426f342fb4d37ee912016e2232c90531 tuned; diff -r 37b53813426f -r 0afb01666df2 src/Tools/Graphview/src/graph_panel.scala --- a/src/Tools/Graphview/src/graph_panel.scala Mon Dec 10 17:44:17 2012 +0100 +++ b/src/Tools/Graphview/src/graph_panel.scala Mon Dec 10 19:17:16 2012 +0100 @@ -47,7 +47,7 @@ private val gfx_aux = new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics - gfx_aux.setFont(visualizer.Font()) + gfx_aux.setFont(visualizer.font) gfx_aux.setRenderingHints(visualizer.rendering_hints) def node(at: Point2D): Option[String] = diff -r 37b53813426f -r 0afb01666df2 src/Tools/Graphview/src/visualizer.scala --- 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,