# HG changeset patch # User wenzelm # Date 1420581060 -3600 # Node ID e8189de55b65413b7b40e6652752069f1870839b # Parent 7009e5fa5cd350bee76d7f56f9fe9d06bdd37441# Parent 9479766b94180fdd444dceed03395fc75691dc52 merged diff -r 7009e5fa5cd3 -r e8189de55b65 NEWS --- a/NEWS Tue Jan 06 09:59:43 2015 +0100 +++ b/NEWS Tue Jan 06 22:51:00 2015 +0100 @@ -30,6 +30,9 @@ *** Prover IDE -- Isabelle/Scala/jEdit *** +* Old graph browser (Java/AWT 1.0) is superseded by improved graphview +panel, which also includes PDF output. + * Improved folding mode "isabelle" based on Isar syntax. Alternatively, the "sidekick" mode may be used for document structure. diff -r 7009e5fa5cd3 -r e8189de55b65 src/Pure/Tools/class_deps.ML --- a/src/Pure/Tools/class_deps.ML Tue Jan 06 09:59:43 2015 +0100 +++ b/src/Pure/Tools/class_deps.ML Tue Jan 06 22:51:00 2015 +0100 @@ -13,7 +13,7 @@ structure Class_Deps: CLASS_DEPS = struct -fun gen_visualize prep_sort ctxt raw_super raw_sub = +fun gen_class_deps prep_sort ctxt raw_super raw_sub = let val thy = Proof_Context.theory_of ctxt; val super = prep_sort ctxt raw_super; @@ -36,8 +36,8 @@ |> Graph_Display.display_graph end; -val class_deps = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); -val class_deps_cmd = gen_visualize Syntax.read_sort; +val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of); +val class_deps_cmd = gen_class_deps Syntax.read_sort; val _ = Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies" diff -r 7009e5fa5cd3 -r e8189de55b65 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Tue Jan 06 09:59:43 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Tue Jan 06 22:51:00 2015 +0100 @@ -26,7 +26,7 @@ override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { override def getToolTipText(event: java.awt.event.MouseEvent): String = - find_visible_node(Transform.pane_to_graph_coordinates(event.getPoint)) match { + visualizer.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match { case Some(node) => visualizer.model.full_graph.get_node(node) match { case Nil => null @@ -44,10 +44,6 @@ peer.getVerticalScrollBar.setUnitIncrement(10) - def find_visible_node(at: Point2D): Option[Graph_Display.Node] = - visualizer.visible_graph.keys_iterator.find(node => - Shapes.Node.shape(visualizer, node).contains(at)) - def refresh() { if (paint_panel != null) { @@ -72,7 +68,7 @@ def apply_layout() { - visualizer.Coordinates.update_layout() + visualizer.update_layout() repaint() } @@ -80,7 +76,7 @@ { def set_preferred_size() { - val box = visualizer.Coordinates.bounding_box() + val box = visualizer.bounding_box() val s = Transform.scale_discrete preferredSize = @@ -135,7 +131,7 @@ def apply() = { - val box = visualizer.Coordinates.bounding_box() + val box = visualizer.bounding_box() val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) at.translate(- box.x, - box.y) at @@ -146,7 +142,7 @@ if (visualizer.visible_graph.is_empty) rescale(1.0) else { - val box = visualizer.Coordinates.bounding_box() + val box = visualizer.bounding_box() rescale((size.width / box.width) min (size.height / box.height)) } } @@ -163,7 +159,7 @@ object Mouse_Interaction { - private var draginfo: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]) = null + private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = null val react: PartialFunction[Event, Unit] = { @@ -175,19 +171,11 @@ case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e) } - def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] = - visualizer.visible_graph.edges_iterator.map(edge => - visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten. - collectFirst({ - case (edge, (d, index)) - if Shapes.Dummy.shape(visualizer, d).contains(at) => (edge, index) - }) - def pressed(at: Point) { val c = Transform.pane_to_graph_coordinates(at) val l = - find_visible_node(c) match { + visualizer.find_node(c) match { case Some(node) => if (visualizer.Selection.contains(node)) visualizer.Selection.get() else List(node) @@ -195,11 +183,7 @@ } val d = l match { - case Nil => - dummy(c) match { - case Some(d) => List(d) - case None => Nil - } + case Nil => visualizer.find_dummy(c).toList case _ => Nil } draginfo = (at, l, d) @@ -211,7 +195,7 @@ def left_click() { - (find_visible_node(c), m) match { + (visualizer.find_node(c), m) match { case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node) case (None, Key.Modifier.Control) => @@ -228,7 +212,7 @@ def right_click() { - val menu = Popups(panel, find_visible_node(c), visualizer.Selection.get()) + val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get()) menu.show(panel.peer, at.x, at.y) } @@ -238,7 +222,7 @@ } } - def drag(info: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]), to: Point) + def drag(info: (Point, List[Graph_Display.Node], List[Layout.Dummy]), to: Point) { val (from, p, d) = info @@ -247,15 +231,14 @@ (p, d) match { case (Nil, Nil) => val r = panel.peer.getViewport.getViewRect - r.translate(-dx, -dy) - + r.translate(- dx, - dy) paint_panel.peer.scrollRectToVisible(r) case (Nil, ds) => - ds.foreach(d => visualizer.Coordinates.translate_dummy(d, dx / s, dy / s)) + ds.foreach(d => visualizer.translate_vertex(d, dx / s, dy / s)) case (ls, _) => - ls.foreach(l => visualizer.Coordinates.translate_node(l, dx / s, dy / s)) + ls.foreach(l => visualizer.translate_vertex(Layout.Node(l), dx / s, dy / s)) } } } diff -r 7009e5fa5cd3 -r e8189de55b65 src/Tools/Graphview/layout.scala --- a/src/Tools/Graphview/layout.scala Tue Jan 06 09:59:43 2015 +0100 +++ b/src/Tools/Graphview/layout.scala Tue Jan 06 22:51:00 2015 +0100 @@ -2,7 +2,7 @@ Author: Markus Kaiser, TU Muenchen Author: Makarius -DAG layout algorithm, according to: +DAG layout according to: Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing, DIMACS International Workshop (GD'94), Springer LNCS 894, 1995. @@ -19,105 +19,185 @@ object Layout { + /* graph structure */ + + object Vertex + { + object Ordering extends scala.math.Ordering[Vertex] + { + def compare(v1: Vertex, v2: Vertex): Int = + (v1, v2) match { + case (_: Node, _: Dummy) => -1 + case (_: Dummy, _: Node) => 1 + case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b) + case (Dummy(a1, a2, i), Dummy(b1, b2, j)) => + Graph_Display.Node.Ordering.compare(a1, b1) match { + case 0 => + Graph_Display.Node.Ordering.compare(a2, b2) match { + case 0 => i compare j + case ord => ord + } + case ord => ord + } + } + } + } + + sealed abstract class Vertex + case class Node(node: Graph_Display.Node) extends Vertex + case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex + object Point { val zero: Point = Point(0.0, 0.0) } case class Point(x: Double, y: Double) - private type Key = Graph_Display.Node - private type Coordinates = Map[Key, Point] - private type Level = List[Key] - private type Levels = List[Level] + type Graph = isabelle.Graph[Vertex, Point] + + def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph = + isabelle.Graph.make(entries)(Vertex.Ordering) + + val empty_graph: Graph = make_graph(Nil) + + + /* vertex x coordinate */ + + private def vertex_left(metrics: Metrics, graph: Graph, v: Vertex): Double = + graph.get_node(v).x - metrics.box_width2(v) + + private def vertex_right(metrics: Metrics, graph: Graph, v: Vertex): Double = + graph.get_node(v).x + metrics.box_width2(v) - val empty: Layout = - new Layout(Metrics.default, Graph_Display.empty_graph, Map.empty, Map.empty) + private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph = + if (dx == 0.0) graph else graph.map_node(v, p => Point(p.x + dx, p.y)) + + /* layout */ + + val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph) + + val minimize_crossings_iterations = 40 val pendulum_iterations = 10 - val minimize_crossings_iterations = 40 + val rubberband_iterations = 10 + - def make(metrics: Metrics, visible_graph: Graph_Display.Graph): Layout = + private type Levels = Map[Vertex, Int] + private val empty_levels: Levels = Map.empty + + def make(metrics: Metrics, input_graph: Graph_Display.Graph): Layout = { - if (visible_graph.is_empty) empty + if (input_graph.is_empty) empty else { - val initial_levels = level_map(visible_graph) + /* initial graph */ + + val initial_graph = + make_graph( + input_graph.iterator.map( + { case (a, (_, (_, bs))) => ((Node(a), Point.zero), bs.toList.map(Node(_))) }).toList) + + val initial_levels: Levels = + (empty_levels /: initial_graph.topological_order) { + case (levels, vertex) => + val level = + 1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) } + levels + (vertex -> level) + } + - val (dummy_graph, dummies, dummy_levels) = - ((visible_graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: - visible_graph.edges_iterator) { - case ((graph, dummies, levels), (from, to)) => - if (levels(to) - levels(from) <= 1) (graph, dummies, levels) + /* graph with dummies */ + + val (dummy_graph, dummy_levels) = + ((initial_graph, initial_levels) /: input_graph.edges_iterator) { + case ((graph, levels), (node1, node2)) => + val v1 = Node(node1); val l1 = levels(v1) + val v2 = Node(node2); val l2 = levels(v2) + if (l2 - l1 <= 1) (graph, levels) else { - val (graph1, ds, levels1) = add_dummies(graph, from, to, levels) - (graph1, dummies + ((from, to) -> ds), levels1) + val dummies_levels = + (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex } + yield (Dummy(node1, node2, i), l)).toList + val dummies = dummies_levels.map(_._1) + + val levels1 = (levels /: dummies_levels)(_ + _) + val graph1 = + ((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /: + (v1 :: dummies ::: List(v2)).sliding(2)) { + case (g, List(a, b)) => g.add_edge(a, b) } + (graph1, levels1) } } + + /* minimize edge crossings and initial coordinates */ + val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) - val initial_coordinates: Coordinates = - (((Map.empty[Key, Point], 0.0) /: levels) { - case ((coords1, y), level) => - ((((coords1, 0.0) /: level) { - case ((coords2, x), key) => - val w2 = metrics.box_width2(key) - (coords2 + (key -> Point(x + w2, y)), x + 2 * w2 + metrics.box_gap) + val levels_graph: Graph = + (((dummy_graph, 0.0) /: levels) { + case ((graph, y), level) => + ((((graph, 0.0) /: level) { + case ((g, x), v) => + val w2 = metrics.box_width2(v) + (g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap) })._1, y + metrics.box_height(level.length)) })._1 - val coords = pendulum(metrics, dummy_graph, levels, initial_coordinates) + /* pendulum/rubberband layout */ - val dummy_coords = - (Map.empty[(Key, Key), List[Point]] /: dummies.keys) { - case (map, key) => map + (key -> dummies(key).map(coords(_))) - } + val output_graph = + rubberband(metrics, levels, + pendulum(metrics, levels, levels_graph)) - new Layout(metrics, visible_graph, coords, dummy_coords) + new Layout(metrics, input_graph, output_graph) } } - def add_dummies(graph: Graph_Display.Graph, from: Key, to: Key, levels: Map[Key, Int]) - : (Graph_Display.Graph, List[Key], Map[Key, Int]) = + + /** edge crossings **/ + + private type Level = List[Vertex] + + private def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] = { - val ds = - ((levels(from) + 1) until levels(to)).map(l => { - // FIXME !? - val ident = "%s$%s$%d".format(from.ident, to.ident, l) - Graph_Display.Node(" ", ident) - }).toList + def resort(parent: Level, child: Level, top_down: Boolean): Level = + child.map(v => { + val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) + val weight = + (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) + (v, weight) + }).sortBy(_._2).map(_._1) - val ls = - (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { - case (ls, (l, d)) => ls + (d -> l) - } - - val graph1 = (graph /: ds)(_.new_node(_, Nil)) - val graph2 = - (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { - case (g, List(x, y)) => g.add_edge(x, y) - } - (graph2, ds, ls) + ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { + case ((old_levels, old_crossings, top_down), _) => + val new_levels = + if (top_down) + (List(old_levels.head) /: old_levels.tail)((tops, bot) => + resort(tops.head, bot, top_down) :: tops).reverse + else { + val rev_old_levels = old_levels.reverse + (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) => + resort(bots.head, top, top_down) :: bots) + } + val new_crossings = count_crossings(graph, new_levels) + if (new_crossings < old_crossings) + (new_levels, new_crossings, !top_down) + else + (old_levels, old_crossings, !top_down) + }._1 } - def level_map(graph: Graph_Display.Graph): Map[Key, Int] = - (Map.empty[Key, Int] /: graph.topological_order) { - (levels, key) => { - val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) } - levels + (key -> lev) - } - } - - def level_list(map: Map[Key, Int]): Levels = + private def level_list(levels: Levels): List[Level] = { - val max_lev = (-1 /: map) { case (m, (_, l)) => m max l } + val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l } val buckets = new Array[Level](max_lev + 1) for (l <- 0 to max_lev) { buckets(l) = Nil } - for ((key, l) <- map) { buckets(l) = key :: buckets(l) } - buckets.iterator.map(_.sorted(Graph_Display.Node.Ordering)).toList + for ((v, l) <- levels) { buckets(l) = v :: buckets(l) } + buckets.iterator.map(_.sorted(Vertex.Ordering)).toList } - def count_crossings(graph: Graph_Display.Graph, levels: Levels): Int = + private def count_crossings(graph: Graph, levels: List[Level]): Int = { - def in_level(ls: Levels): Int = ls match { + def in_level(ls: List[Level]): Int = ls match { case List(top, bot) => top.iterator.zipWithIndex.map { case (outer_parent, outer_parent_index) => @@ -138,58 +218,50 @@ levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum } - def minimize_crossings(graph: Graph_Display.Graph, levels: Levels): Levels = + + + /** pendulum method **/ + + /*This is an auxiliary class which is used by the layout algorithm when + calculating coordinates with the "pendulum method". A "region" is a + group of vertices which "stick together".*/ + private class Region(init: Vertex) { - def resort_level(parent: Level, child: Level, top_down: Boolean): Level = - child.map(k => { - val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) - val weight = - (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) - (k, weight) - }).sortBy(_._2).map(_._1) + var content: List[Vertex] = List(init) - def resort(levels: Levels, top_down: Boolean) = - if (top_down) - (List(levels.head) /: levels.tail)((tops, bot) => - resort_level(tops.head, bot, top_down) :: tops).reverse - else { - val rev_levels = levels.reverse - (List(rev_levels.head) /: rev_levels.tail)((bots, top) => - resort_level(bots.head, top, top_down) :: bots) - } + def distance(metrics: Metrics, graph: Graph, that: Region): Double = + vertex_left(metrics, graph, that.content.head) - + vertex_right(metrics, graph, this.content.last) - + metrics.box_gap - ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { - case ((old_levels, old_crossings, top_down), _) => { - val new_levels = resort(old_levels, top_down) - val new_crossings = count_crossings(graph, new_levels) - if (new_crossings < old_crossings) - (new_levels, new_crossings, !top_down) - else - (old_levels, old_crossings, !top_down) - } - }._1 + def deflection(graph: Graph, top_down: Boolean): Double = + ((for (a <- content.iterator) yield { + val x = graph.get_node(a).x + val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a) + bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1) + }).sum / content.length).round.toDouble + + def move(graph: Graph, dx: Double): Graph = + if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx)) } - def pendulum( - metrics: Metrics, graph: Graph_Display.Graph, - levels: Levels, coords: Map[Key, Point]): Coordinates = + private type Regions = List[List[Region]] + + private def pendulum(metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph = { - type Regions = List[List[Region]] - - def iteration( - coords: Coordinates, regions: Regions, top_down: Boolean): (Coordinates, Regions, Boolean) = + def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) = { - val (coords1, regions1, moved) = - ((coords, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) { - case ((coords, tops, moved), bot) => - val bot1 = collapse(coords, bot, top_down) - val (coords1, moved1) = deflect(coords, bot1, top_down) - (coords1, bot1 :: tops, moved || moved1) + val (graph1, regions1, moved) = + ((graph, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) { + case ((graph, tops, moved), bot) => + val bot1 = collapse(graph, bot, top_down) + val (graph1, moved1) = deflect(graph, bot1, top_down) + (graph1, bot1 :: tops, moved || moved1) } - (coords1, regions1.reverse, moved) + (graph1, regions1.reverse, moved) } - def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] = + def collapse(graph: Graph, level: List[Region], top_down: Boolean): List[Region] = { if (level.size <= 1) level else { @@ -199,16 +271,16 @@ regions_changed = false for (i <- Range(next.length - 1, 0, -1)) { val (r1, r2) = (next(i - 1), next(i)) - val d1 = r1.deflection(graph, coords, top_down) - val d2 = r2.deflection(graph, coords, top_down) + val d1 = r1.deflection(graph, top_down) + val d2 = r2.deflection(graph, top_down) if (// Do regions touch? - r1.distance(metrics, coords, r2) <= 0.0 && + r1.distance(metrics, graph, r2) <= 0.0 && // Do they influence each other? (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0)) { regions_changed = true - r1.nodes = r1.nodes ::: r2.nodes + r1.content = r1.content ::: r2.content next = next.filter(next.indexOf(_) != i) } } @@ -217,101 +289,108 @@ } } - def deflect( - coords: Coordinates, level: List[Region], top_down: Boolean): (Coordinates, Boolean) = + def deflect(graph: Graph, level: List[Region], top_down: Boolean): (Graph, Boolean) = { - ((coords, false) /: (0 until level.length)) { - case ((coords, moved), i) => + ((graph, false) /: (0 until level.length)) { + case ((graph, moved), i) => val r = level(i) - val d = r.deflection(graph, coords, top_down) + val d = r.deflection(graph, top_down) val offset = if (d < 0 && i > 0) - - (level(i - 1).distance(metrics, coords, r) min (- d)) + - (level(i - 1).distance(metrics, graph, r) min (- d)) else if (d >= 0 && i < level.length - 1) - r.distance(metrics, coords, level(i + 1)) min d + r.distance(metrics, graph, level(i + 1)) min d else d - (r.move(coords, offset), moved || d != 0) + (r.move(graph, offset), moved || d != 0) } } - val regions = levels.map(level => level.map(new Region(_))) + val initial_regions = levels.map(level => level.map(new Region(_))) - ((coords, regions, true, true) /: (1 to pendulum_iterations)) { - case ((coords, regions, top_down, moved), _) => + ((levels_graph, initial_regions, true, true) /: (1 to pendulum_iterations)) { + case ((graph, regions, top_down, moved), _) => if (moved) { - val (coords1, regions1, m) = iteration(coords, regions, top_down) - (coords1, regions1, !top_down, m) + val (graph1, regions1, moved1) = iteration(graph, regions, top_down) + (graph1, regions1, !top_down, moved1) } - else (coords, regions, !top_down, moved) + else (graph, regions, !top_down, moved) }._1 } - /*This is an auxiliary class which is used by the layout algorithm when - calculating coordinates with the "pendulum method". A "region" is a - group of nodes which "stick together".*/ - private class Region(node: Key) - { - var nodes: List[Key] = List(node) + + + /** rubberband method **/ - def distance(metrics: Metrics, coords: Coordinates, that: Region): Double = - { - val n1 = this.nodes.last; val x1 = coords(n1).x + metrics.box_width2(n1) - val n2 = that.nodes.head; val x2 = coords(n2).x - metrics.box_width2(n2) - x2 - x1 - metrics.box_gap + private def force_weight(graph: Graph, v: Vertex): Double = + { + val preds = graph.imm_preds(v) + val succs = graph.imm_succs(v) + val n = preds.size + succs.size + if (n == 0) 0.0 + else { + val x = graph.get_node(v).x + ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n } + } - def deflection(graph: Graph_Display.Graph, coords: Coordinates, top_down: Boolean): Double = - ((for (a <- nodes.iterator) yield { - val x = coords(a).x - val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a) - bs.iterator.map(coords(_).x - x).sum / (bs.size max 1) - }).sum / nodes.length).round.toDouble + private def rubberband(metrics: Metrics, levels: List[Level], graph: Graph): Graph = + { + val gap = metrics.box_gap + def left(g: Graph, v: Vertex) = vertex_left(metrics, g, v) + def right(g: Graph, v: Vertex) = vertex_right(metrics, g, v) - def move(coords: Coordinates, dx: Double): Coordinates = - if (dx == 0.0) coords - else - (coords /: nodes) { - case (cs, node) => - val p = cs(node) - cs + (node -> Point(p.x + dx, p.y)) + (graph /: (1 to rubberband_iterations)) { case (graph, _) => + (graph /: levels) { case (graph, level) => + val m = level.length - 1 + (graph /: level.iterator.zipWithIndex) { + case (g, (v, i)) => + val d = force_weight(g, v) + if (d < 0.0 && (i == 0 || right(g, level(i - 1)) + gap < left(g, v) + d) || + d > 0.0 && (i == m || left(g, level(i + 1)) - gap > right(g, v) + d)) + move_vertex(g, v, d.round.toDouble) + else g } + } + } } } final class Layout private( val metrics: Metrics, - val visible_graph: Graph_Display.Graph, - nodes: Map[Graph_Display.Node, Layout.Point], - dummies: Map[Graph_Display.Edge, List[Layout.Point]]) + val input_graph: Graph_Display.Graph, + val output_graph: Layout.Graph) { - /* nodes */ + /* vertex coordinates */ + + def get_vertex(v: Layout.Vertex): Layout.Point = + if (output_graph.defined(v)) output_graph.get_node(v) + else Layout.Point.zero - 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) => - val nodes1 = nodes + (node -> f(p)) - new Layout(metrics, visible_graph, nodes1, dummies) + def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout = + { + if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this + else { + val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dx, p.y + dy)) + new Layout(metrics, input_graph, output_graph1) } + } /* dummies */ - def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = - dummies.getOrElse(edge, Nil) + def dummies_iterator: Iterator[Layout.Point] = + for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p - 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) => - val dummies1 = dummies + (edge -> f(ds)) - new Layout(metrics, visible_graph, nodes, dummies1) + def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] = + new Iterator[Layout.Point] { + private var index = 0 + def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index)) + def next: Layout.Point = + { + val p = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index)) + index += 1 + p + } } - - def dummies_iterator: Iterator[Layout.Point] = - for { (_, ds) <- dummies.iterator; d <- ds.iterator } yield d } diff -r 7009e5fa5cd3 -r e8189de55b65 src/Tools/Graphview/main_panel.scala --- a/src/Tools/Graphview/main_panel.scala Tue Jan 06 09:59:43 2015 +0100 +++ b/src/Tools/Graphview/main_panel.scala Tue Jan 06 22:51:00 2015 +0100 @@ -66,7 +66,7 @@ private def export(file: JFile) { - val box = visualizer.Coordinates.bounding_box() + val box = visualizer.bounding_box() val w = box.width.ceil.toInt val h = box.height.ceil.toInt diff -r 7009e5fa5cd3 -r e8189de55b65 src/Tools/Graphview/metrics.scala --- a/src/Tools/Graphview/metrics.scala Tue Jan 06 09:59:43 2015 +0100 +++ b/src/Tools/Graphview/metrics.scala Tue Jan 06 22:51:00 2015 +0100 @@ -38,8 +38,16 @@ def pad_x: Double = char_width * 1.5 def pad_y: Double = char_width + def dummy_width2: Double = (pad_x / 2).ceil + def box_width2(node: Graph_Display.Node): Double = ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil + + def box_width2(vertex: Layout.Vertex): Double = + vertex match { + case Layout.Node(node) => box_width2(node) + case _: Layout.Dummy => dummy_width2 + } def box_gap: Double = gap.ceil def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil } diff -r 7009e5fa5cd3 -r e8189de55b65 src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala Tue Jan 06 09:59:43 2015 +0100 +++ b/src/Tools/Graphview/shapes.scala Tue Jan 06 22:51:00 2015 +0100 @@ -24,11 +24,11 @@ def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double = { val metrics = visualizer.metrics - val p = visualizer.Coordinates.get_node(node) + val p = visualizer.layout.get_vertex(Layout.Node(node)) val bounds = metrics.string_bounds(node.toString) - val w = bounds.getWidth + metrics.pad_x - val h = bounds.getHeight + metrics.pad_y - new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil) + val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil + val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil + new Rectangle2D.Double(p.x - w2, p.y - h2, 2 * w2, 2 * h2) } def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node) @@ -58,8 +58,8 @@ def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double = { val metrics = visualizer.metrics - val w = metrics.pad_x - new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil) + val w = metrics.dummy_width2 + new Rectangle2D.Double(d.x - w / 2, d.y - w / 2, w, w) } def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point) @@ -74,13 +74,13 @@ { def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) { - val p = visualizer.Coordinates.get_node(edge._1) - val q = visualizer.Coordinates.get_node(edge._2) + val p = visualizer.layout.get_vertex(Layout.Node(edge._1)) + val q = visualizer.layout.get_vertex(Layout.Node(edge._2)) val ds = { 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) + visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) @@ -106,13 +106,13 @@ def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) { - val p = visualizer.Coordinates.get_node(edge._1) - val q = visualizer.Coordinates.get_node(edge._2) + val p = visualizer.layout.get_vertex(Layout.Node(edge._1)) + val q = visualizer.layout.get_vertex(Layout.Node(edge._2)) val ds = { 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) + visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge) diff -r 7009e5fa5cd3 -r e8189de55b65 src/Tools/Graphview/visualizer.scala --- a/src/Tools/Graphview/visualizer.scala Tue Jan 06 09:59:43 2015 +0100 +++ b/src/Tools/Graphview/visualizer.scala Tue Jan 06 22:51:00 2015 +0100 @@ -11,7 +11,7 @@ import isabelle._ import java.awt.{Font, Color, Shape, Graphics2D} -import java.awt.geom.Rectangle2D +import java.awt.geom.{Point2D, Rectangle2D} import javax.swing.JComponent @@ -19,11 +19,59 @@ { visualizer => + + /* layout state */ + // owned by GUI thread - private var layout: Layout = Layout.empty + private var _layout: Layout = Layout.empty + def layout: Layout = _layout def metrics: Metrics = layout.metrics - def visible_graph: Graph_Display.Graph = layout.visible_graph + def visible_graph: Graph_Display.Graph = layout.input_graph + + def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit = + _layout = _layout.translate_vertex(v, dx, dy) + + def find_node(at: Point2D): Option[Graph_Display.Node] = + layout.output_graph.iterator.collectFirst({ + case (Layout.Node(node), _) if Shapes.Node.shape(visualizer, node).contains(at) => node + }) + + def find_dummy(at: Point2D): Option[Layout.Dummy] = + layout.output_graph.iterator.collectFirst({ + case (dummy: Layout.Dummy, (d, _)) if Shapes.Dummy.shape(visualizer, d).contains(at) => dummy + }) + + def bounding_box(): Rectangle2D.Double = + { + var x0 = 0.0 + var y0 = 0.0 + var x1 = 0.0 + var y1 = 0.0 + ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++ + (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))). + foreach(rect => { + x0 = x0 min rect.getMinX + y0 = y0 min rect.getMinY + x1 = x1 max rect.getMaxX + y1 = y1 max rect.getMaxY + }) + val gap = metrics.gap + x0 = (x0 - gap).floor + y0 = (y0 - gap).floor + x1 = (x1 + gap).ceil + y1 = (y1 + gap).ceil + new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) + } + + def update_layout() + { + val metrics = Metrics(make_font()) + val visible_graph = model.make_visible_graph() + + // FIXME avoid expensive operation on GUI thread + _layout = Layout.make(metrics, visible_graph) + } /* tooltips */ @@ -85,60 +133,6 @@ Shapes.Node.paint(gfx, visualizer, node) } - object Coordinates - { - 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 translate_node(node: Graph_Display.Node, dx: Double, dy: Double) - { - layout = layout.map_node(node, p => Layout.Point(p.x + dx, p.y + dy)) - } - - def translate_dummy(d: (Graph_Display.Edge, Int), dx: Double, dy: Double) - { - 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() - { - val metrics = Metrics(make_font()) - val visible_graph = model.make_visible_graph() - - // FIXME avoid expensive operation on GUI thread - layout = Layout.make(metrics, visible_graph) - } - - def bounding_box(): Rectangle2D.Double = - { - var x0 = 0.0 - var y0 = 0.0 - var x1 = 0.0 - var y1 = 0.0 - ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++ - (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))). - foreach(rect => { - x0 = x0 min rect.getMinX - y0 = y0 min rect.getMinY - x1 = x1 max rect.getMaxX - y1 = y1 max rect.getMaxY - }) - val gap = metrics.gap - x0 = (x0 - gap).floor - y0 = (y0 - gap).floor - x1 = (x1 + gap).ceil - y1 = (y1 + gap).ceil - new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) - } - } - object Selection { // owned by GUI thread