--- a/src/Tools/Graphview/graph_panel.scala Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Sun Jan 04 21:01:27 2015 +0100
@@ -164,9 +164,7 @@
object Mouse_Interaction
{
- type Dummy = (Graph_Display.Edge, Int)
-
- private var draginfo: (Point, List[Graph_Display.Node], List[Dummy]) = null
+ private var draginfo: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]) = null
val react: PartialFunction[Event, Unit] =
{
@@ -178,19 +176,20 @@
case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e)
}
- def dummy(at: Point2D): Option[Dummy] =
+ def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] =
{
val m = visualizer.metrics()
visualizer.model.make_visible_graph().edges_iterator.map(
- edge => visualizer.Coordinates(edge).zipWithIndex.map((edge, _))).flatten.find(
- {
- case (_, ((x, y), _)) =>
- visualizer.Drawer.shape(m, Graph_Display.Node.dummy).
- contains(at.getX() - x, at.getY() - y)
- }) match {
- case None => None
- case Some((edge, (_, index))) => Some((edge, index))
- }
+ edge =>
+ visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find(
+ {
+ case (_, (p, _)) =>
+ visualizer.Drawer.shape(m, Graph_Display.Node.dummy).
+ contains(at.getX() - p.x, at.getY() - p.y)
+ }) match {
+ case None => None
+ case Some((edge, (_, index))) => Some((edge, index))
+ }
}
def pressed(at: Point)
@@ -248,9 +247,9 @@
}
}
- def drag(draginfo: (Point, List[Graph_Display.Node], List[Dummy]), to: Point)
+ def drag(info: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]), to: Point)
{
- val (from, p, d) = draginfo
+ val (from, p, d) = info
val s = Transform.scale_discrete
val (dx, dy) = (to.x - from.x, to.y - from.y)
@@ -262,10 +261,10 @@
paint_panel.peer.scrollRectToVisible(r)
case (Nil, ds) =>
- ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s)))
+ ds.foreach(d => visualizer.Coordinates.translate_dummy(d, dx / s, dy / s))
case (ls, _) =>
- ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s)))
+ ls.foreach(l => visualizer.Coordinates.translate_node(l, dx / s, dy / s))
}
}
}
--- a/src/Tools/Graphview/layout.scala Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/layout.scala Sun Jan 04 21:01:27 2015 +0100
@@ -17,19 +17,17 @@
import isabelle._
-final case class Layout(
- nodes: Layout.Coordinates,
- dummies: Map[Graph_Display.Edge, List[Layout.Point]])
-
object Layout
{
- type Key = Graph_Display.Node
- type Point = (Double, Double)
- type Coordinates = Map[Key, Point]
- type Level = List[Key]
- type Levels = List[Level]
+ object Point { val zero: Point = Point(0.0, 0.0) }
+ case class Point(x: Double, y: Double)
- val empty = Layout(Map.empty, Map.empty)
+ private type Key = Graph_Display.Node
+ private type Coordinates = Map[Key, Point]
+ private type Level = List[Key]
+ private type Levels = List[Level]
+
+ val empty = new Layout(Map.empty, Map.empty)
val pendulum_iterations = 10
val minimize_crossings_iterations = 40
@@ -68,7 +66,7 @@
(((Map.empty[Key, Point], 0.0) /: levels) {
case ((coords1, y), level) =>
((((coords1, 0.0) /: level) {
- case ((coords2, x), key) => (coords2 + (key -> (x, y)), x + box_distance)
+ case ((coords2, x), key) => (coords2 + (key -> Point(x, y)), x + box_distance)
})._1, y + box_height(level))
})._1
@@ -79,7 +77,7 @@
case (map, key) => map + (key -> dummies(key).map(coords(_)))
}
- Layout(coords, dummy_coords)
+ new Layout(coords, dummy_coords)
}
}
@@ -274,8 +272,8 @@
{
var nodes: List[Key] = List(node)
- def left(coords: Coordinates): Double = nodes.iterator.map(coords(_)._1).min
- def right(coords: Coordinates): Double = nodes.iterator.map(coords(_)._1).max
+ def left(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).min
+ def right(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).max
def distance(coords: Coordinates, to: Region): Double =
math.abs(left(coords) - to.left(coords)) min
@@ -284,15 +282,40 @@
def deflection(coords: Coordinates, top_down: Boolean): Double =
(for {
k <- nodes.iterator
- x = coords(k)._1
+ x = coords(k).x
as = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
- } yield as.iterator.map(coords(_)._1 - x).sum / (as.size max 1)).sum / nodes.length
+ } yield as.iterator.map(coords(_).x - x).sum / (as.size max 1)).sum / nodes.length
- def move(coords: Coordinates, by: Double): Coordinates =
+ def move(coords: Coordinates, dx: Double): Coordinates =
(coords /: nodes) {
case (cs, node) =>
- val (x, y) = cs(node)
- cs + (node -> (x + by, y))
+ val p = cs(node)
+ cs + (node -> Point(p.x + dx, p.y))
}
}
}
+
+final class Layout private(
+ nodes: Map[Graph_Display.Node, Layout.Point],
+ dummies: Map[Graph_Display.Edge, List[Layout.Point]])
+{
+ def get_node(node: Graph_Display.Node): Layout.Point =
+ nodes.getOrElse(node, Layout.Point.zero)
+
+ def map_node(node: Graph_Display.Node, f: Layout.Point => Layout.Point): Layout =
+ nodes.get(node) match {
+ case None => this
+ case Some(p) => new Layout(nodes + (node -> f(p)), dummies)
+ }
+
+
+ def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] =
+ dummies.getOrElse(edge, Nil)
+
+ def map_dummies(edge: Graph_Display.Edge, f: List[Layout.Point] => List[Layout.Point]): Layout =
+ dummies.get(edge) match {
+ case None => this
+ case Some(ds) => new Layout(nodes, dummies + (edge -> f(ds)))
+ }
+}
+
--- a/src/Tools/Graphview/shapes.scala Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala Sun Jan 04 21:01:27 2015 +0100
@@ -24,11 +24,11 @@
def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node)
: Rectangle2D.Double =
{
- val (x, y) = visualizer.Coordinates(node)
+ val p = visualizer.Coordinates.get_node(node)
val bounds = m.string_bounds(node.toString)
val w = bounds.getWidth + m.pad
val h = bounds.getHeight + m.pad
- new Rectangle2D.Double((x - (w / 2)).floor, (y - (h / 2)).floor, w.ceil, h.ceil)
+ new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil)
}
def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
@@ -81,28 +81,23 @@
def paint(gfx: Graphics2D, visualizer: Visualizer,
edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
{
- val (fx, fy) = visualizer.Coordinates(edge._1)
- val (tx, ty) = visualizer.Coordinates(edge._2)
+ val p = visualizer.Coordinates.get_node(edge._1)
+ val q = visualizer.Coordinates.get_node(edge._2)
val ds =
{
- val min = fy min ty
- val max = fy max ty
- visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
+ val a = p.y min q.y
+ val b = p.y max q.y
+ visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
}
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
- path.moveTo(fx, fy)
- ds.foreach({ case (x, y) => path.lineTo(x, y) })
- path.lineTo(tx, ty)
+ path.moveTo(p.x, p.y)
+ ds.foreach(d => path.lineTo(d.x, d.y))
+ path.lineTo(q.x, q.y)
- if (dummies) {
- ds.foreach({
- case (x, y) => {
- val at = AffineTransform.getTranslateInstance(x, y)
- Dummy.paint_transformed(gfx, visualizer, at)
- }
- })
- }
+ if (dummies)
+ ds.foreach(d =>
+ Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
gfx.setStroke(default_stroke)
gfx.setColor(visualizer.edge_color(edge))
@@ -121,48 +116,45 @@
def paint(gfx: Graphics2D, visualizer: Visualizer,
edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
{
- val (fx, fy) = visualizer.Coordinates(edge._1)
- val (tx, ty) = visualizer.Coordinates(edge._2)
+ val p = visualizer.Coordinates.get_node(edge._1)
+ val q = visualizer.Coordinates.get_node(edge._2)
val ds =
{
- val min = fy min ty
- val max = fy max ty
- visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
+ val a = p.y min q.y
+ val b = p.y max q.y
+ visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
}
if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge, head, dummies)
else {
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
- path.moveTo(fx, fy)
+ path.moveTo(p.x, p.y)
- val coords = ((fx, fy) :: ds ::: List((tx, ty)))
- val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
+ val coords = p :: ds ::: List(q)
+ val dx = coords(2).x - coords(0).x
+ val dy = coords(2).y - coords(0).y
val (dx2, dy2) =
- ((dx, dy) /: coords.sliding(3))({
- case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => {
- val (dx2, dy2) = (rx - lx, ry - ly)
-
- path.curveTo(lx + slack * dx , ly + slack * dy,
- mx - slack * dx2, my - slack * dy2,
- mx , my)
+ ((dx, dy) /: coords.sliding(3)) {
+ case ((dx, dy), List(l, m, r)) =>
+ val dx2 = r.x - l.x
+ val dy2 = r.y - l.y
+ path.curveTo(
+ l.x + slack * dx, l.y + slack * dy,
+ m.x - slack * dx2, m.y - slack * dy2,
+ m.x, m.y)
(dx2, dy2)
- }
- })
+ }
- val (lx, ly) = ds.last
- path.curveTo(lx + slack * dx2, ly + slack * dy2,
- tx - slack * dx2, ty - slack * dy2,
- tx , ty)
+ val l = ds.last
+ path.curveTo(
+ l.x + slack * dx2, l.y + slack * dy2,
+ q.x - slack * dx2, q.y - slack * dy2,
+ q.x, q.y)
- if (dummies) {
- ds.foreach({
- case (x, y) => {
- val at = AffineTransform.getTranslateInstance(x, y)
- Dummy.paint_transformed(gfx, visualizer, at)
- }
- })
- }
+ if (dummies)
+ ds.foreach(d =>
+ Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
gfx.setStroke(default_stroke)
gfx.setColor(visualizer.edge_color(edge))
--- a/src/Tools/Graphview/visualizer.scala Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala Sun Jan 04 21:01:27 2015 +0100
@@ -103,44 +103,27 @@
object Coordinates
{
+ // owned by GUI thread
private var layout = Layout.empty
- def apply(node: Graph_Display.Node): (Double, Double) =
- layout.nodes.getOrElse(node, (0.0, 0.0))
+ def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node)
+ def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge)
- def apply(edge: Graph_Display.Edge): List[(Double, Double)] =
- layout.dummies.getOrElse(edge, Nil)
-
- def reposition(node: Graph_Display.Node, to: (Double, Double))
+ def translate_node(node: Graph_Display.Node, dx: Double, dy: Double)
{
- layout = layout.copy(nodes = layout.nodes + (node -> to))
+ layout = layout.map_node(node, p => Layout.Point(p.x + dx, p.y + dy))
}
- def reposition(d: (Graph_Display.Edge, Int), to: (Double, Double))
+ def translate_dummy(d: (Graph_Display.Edge, Int), dx: Double, dy: Double)
{
- val (e, index) = d
- layout.dummies.get(e) match {
- case None =>
- case Some(ds) =>
- layout = layout.copy(dummies =
- layout.dummies + (e ->
- (ds.zipWithIndex :\ List.empty[(Double, Double)]) {
- case ((t, i), n) => if (index == i) to :: n else t :: n
- }))
- }
- }
-
- def translate(node: Graph_Display.Node, by: (Double, Double))
- {
- val ((x, y), (dx, dy)) = (Coordinates(node), by)
- reposition(node, (x + dx, y + dy))
- }
-
- def translate(d: (Graph_Display.Edge, Int), by: (Double, Double))
- {
- val ((e, i), (dx, dy)) = (d, by)
- val (x, y) = apply(e)(i)
- reposition(d, (x + dx, y + dy))
+ val (edge, index) = d
+ layout = layout.map_dummies(edge,
+ ds => {
+ val p = ds(index)
+ (ds.zipWithIndex :\ List.empty[Layout.Point]) {
+ case ((t, i), n) => if (index == i) Layout.Point(p.x + dx, p.y + dy) :: n else t :: n
+ }
+ })
}
def update_layout()