# HG changeset patch # User wenzelm # Date 1421615033 -3600 # Node ID ea163bf8ad22d1b6e9a617ae95b81bbb0751087c # Parent fc909f7e7ce51798937c442ea0db902beb229aed misc tuning; diff -r fc909f7e7ce5 -r ea163bf8ad22 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Sun Jan 18 21:35:54 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Sun Jan 18 22:03:53 2015 +0100 @@ -22,6 +22,9 @@ { panel => + + /* tooltips */ + tooltip = "" override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { @@ -36,33 +39,32 @@ } } + + /* scrolling */ + horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always verticalScrollBarPolicy = ScrollPane.BarPolicy.Always peer.getVerticalScrollBar.setUnitIncrement(10) - def refresh() + def scroll_to_node(node: Graph_Display.Node) { - if (paint_panel != null) { - paint_panel.set_preferred_size() - paint_panel.repaint() - } + val gap = visualizer.metrics.gap + val info = visualizer.layout.get_node(node) + + val t = Transform() + val p = + t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null) + val q = + t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null) + + paint_panel.peer.scrollRectToVisible( + new Rectangle(p.getX.toInt, p.getY.toInt, + (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt)) } - def fit_to_window() - { - Transform.fit_to_window() - refresh() - } - val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) } - - def rescale(s: Double) - { - Transform.scale = s - if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt) - refresh() - } + /* painting */ private class Paint_Panel extends Panel { @@ -90,38 +92,33 @@ private val paint_panel = new Paint_Panel contents = paint_panel - listenTo(mouse.moves) - listenTo(mouse.clicks) - reactions += Mouse_Interaction.react - reactions += + def refresh() { - case MousePressed(_, _, _, _, _) => repaint() - case MouseDragged(_, _, _) => repaint() - case MouseClicked(_, _, _, _, _) => repaint() + if (paint_panel != null) { + paint_panel.set_preferred_size() + paint_panel.repaint() + } } - visualizer.model.Colors.events += { case _ => repaint() } - visualizer.model.Mutators.events += { case _ => repaint() } + def fit_to_window() + { + Transform.fit_to_window() + refresh() + } + + val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) } + + def rescale(s: Double) + { + Transform.scale = s + if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt) + refresh() + } rescale(1.0) - def scroll_to_node(node: Graph_Display.Node) - { - val gap = visualizer.metrics.gap - val info = visualizer.layout.get_node(node) - - val t = Transform() - val p = - t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null) - val q = - t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null) - - paint_panel.peer.scrollRectToVisible( - new Rectangle(p.getX.toInt, p.getY.toInt, - (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt)) - } - + /* transform */ private object Transform { @@ -166,19 +163,31 @@ } } - object Mouse_Interaction - { - private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = null + + /* interaction */ - val react: PartialFunction[Event, Unit] = - { - case MousePressed(_, p, _, _, _) => pressed(p) - case MouseDragged(_, to, _) => - drag(draginfo, to) - val (_, p, d) = draginfo - draginfo = (to, p, d) - case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e) - } + listenTo(mouse.moves) + listenTo(mouse.clicks) + reactions += + { + case MousePressed(_, p, _, _, _) => + Mouse_Interaction.pressed(p) + repaint() + case MouseDragged(_, to, _) => + Mouse_Interaction.dragged(to) + repaint() + case e @ MouseClicked(_, p, m, n, _) => + Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer)) + repaint() + } + + visualizer.model.Colors.events += { case _ => repaint() } + visualizer.model.Mutators.events += { case _ => repaint() } + + private object Mouse_Interaction + { + private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = + (new Point(0, 0), Nil, Nil) def pressed(at: Point) { @@ -198,45 +207,14 @@ draginfo = (at, l, d) } - def click(at: Point, m: Key.Modifiers, clicks: Int, e: MouseEvent) + def dragged(to: Point) { - val c = Transform.pane_to_graph_coordinates(at) - - def left_click() - { - (visualizer.find_node(c), m) match { - case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node) - case (None, Key.Modifier.Control) => - - case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node) - case (None, Key.Modifier.Shift) => - - case (Some(node), _) => - visualizer.Selection.clear() - visualizer.Selection.add(node) - case (None, _) => - visualizer.Selection.clear() - } - } - - def right_click() - { - val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get()) - menu.show(panel.peer, at.x, at.y) - } - - if (clicks < 2) { - if (SwingUtilities.isRightMouseButton(e.peer)) right_click() - else left_click() - } - } - - def drag(info: (Point, List[Graph_Display.Node], List[Layout.Dummy]), to: Point) - { - val (from, p, d) = info + val (from, p, d) = draginfo val s = Transform.scale_discrete - val (dx, dy) = (to.x - from.x, to.y - from.y) + val dx = to.x - from.x + val dy = to.y - from.y + (p, d) match { case (Nil, Nil) => val r = panel.peer.getViewport.getViewRect @@ -249,6 +227,35 @@ case (ls, _) => ls.foreach(l => visualizer.translate_vertex(Layout.Node(l), dx / s, dy / s)) } + + draginfo = (to, p, d) + } + + def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean) + { + val c = Transform.pane_to_graph_coordinates(at) + + if (clicks < 2) { + if (right_click) { + val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get()) + menu.show(panel.peer, at.x, at.y) + } + else { + (visualizer.find_node(c), m) match { + case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node) + case (None, Key.Modifier.Control) => + + case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node) + case (None, Key.Modifier.Shift) => + + case (Some(node), _) => + visualizer.Selection.clear() + visualizer.Selection.add(node) + case (None, _) => + visualizer.Selection.clear() + } + } + } } } }