# HG changeset patch # User wenzelm # Date 1420401687 -3600 # Node ID 5cd92c743958b54daeed592320027bfb79161487 # Parent 5e72808149165a064e3e732040986399d873c637 explicit Layout.Point; tuned signature; tuned; diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/graph_panel.scala --- 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)) } } } diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/layout.scala --- 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))) + } +} + diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/shapes.scala --- 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)) diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/visualizer.scala --- 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()