tuned signature;
authorwenzelm
Tue Jan 06 17:08:18 2015 +0100 (2015-01-06)
changeset 59305b5e33012180e
parent 59304 848e27e4ac37
child 59306 cd2a0c14fe66
tuned signature;
src/Tools/Graphview/graph_panel.scala
src/Tools/Graphview/layout.scala
src/Tools/Graphview/visualizer.scala
     1.1 --- a/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:43:17 2015 +0100
     1.2 +++ b/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 17:08:18 2015 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5    override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
     1.6      override def getToolTipText(event: java.awt.event.MouseEvent): String =
     1.7 -      find_visible_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
     1.8 +      visualizer.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
     1.9          case Some(node) =>
    1.10            visualizer.model.full_graph.get_node(node) match {
    1.11              case Nil => null
    1.12 @@ -44,10 +44,6 @@
    1.13  
    1.14    peer.getVerticalScrollBar.setUnitIncrement(10)
    1.15  
    1.16 -  def find_visible_node(at: Point2D): Option[Graph_Display.Node] =
    1.17 -    visualizer.visible_graph.keys_iterator.find(node =>
    1.18 -      Shapes.Node.shape(visualizer, node).contains(at))
    1.19 -
    1.20    def refresh()
    1.21    {
    1.22      if (paint_panel != null) {
    1.23 @@ -175,14 +171,11 @@
    1.24        case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e)
    1.25      }
    1.26  
    1.27 -    def dummy(at: Point2D): Option[Layout.Dummy] =
    1.28 -      visualizer.layout.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
    1.29 -
    1.30      def pressed(at: Point)
    1.31      {
    1.32        val c = Transform.pane_to_graph_coordinates(at)
    1.33        val l =
    1.34 -        find_visible_node(c) match {
    1.35 +        visualizer.find_node(c) match {
    1.36            case Some(node) =>
    1.37              if (visualizer.Selection.contains(node)) visualizer.Selection.get()
    1.38              else List(node)
    1.39 @@ -190,11 +183,7 @@
    1.40          }
    1.41        val d =
    1.42          l match {
    1.43 -          case Nil =>
    1.44 -            dummy(c) match {
    1.45 -              case Some(d) => List(d)
    1.46 -              case None => Nil
    1.47 -            }
    1.48 +          case Nil => visualizer.find_dummy(c).toList
    1.49            case _ => Nil
    1.50          }
    1.51        draginfo = (at, l, d)
    1.52 @@ -206,7 +195,7 @@
    1.53  
    1.54        def left_click()
    1.55        {
    1.56 -        (find_visible_node(c), m) match {
    1.57 +        (visualizer.find_node(c), m) match {
    1.58            case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
    1.59            case (None, Key.Modifier.Control) =>
    1.60  
    1.61 @@ -223,7 +212,7 @@
    1.62  
    1.63        def right_click()
    1.64        {
    1.65 -        val menu = Popups(panel, find_visible_node(c), visualizer.Selection.get())
    1.66 +        val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get())
    1.67          menu.show(panel.peer, at.x, at.y)
    1.68        }
    1.69  
     2.1 --- a/src/Tools/Graphview/layout.scala	Tue Jan 06 16:43:17 2015 +0100
     2.2 +++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 17:08:18 2015 +0100
     2.3 @@ -332,9 +332,6 @@
     2.4  
     2.5    /* dummies */
     2.6  
     2.7 -  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
     2.8 -    output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d })
     2.9 -
    2.10    def dummies_iterator: Iterator[Layout.Point] =
    2.11      for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p
    2.12  
     3.1 --- a/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:43:17 2015 +0100
     3.2 +++ b/src/Tools/Graphview/visualizer.scala	Tue Jan 06 17:08:18 2015 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4  import isabelle._
     3.5  
     3.6  import java.awt.{Font, Color, Shape, Graphics2D}
     3.7 -import java.awt.geom.Rectangle2D
     3.8 +import java.awt.geom.{Point2D, Rectangle2D}
     3.9  import javax.swing.JComponent
    3.10  
    3.11  
    3.12 @@ -32,6 +32,16 @@
    3.13    def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
    3.14      _layout = _layout.translate_vertex(v, dx, dy)
    3.15  
    3.16 +  def find_node(at: Point2D): Option[Graph_Display.Node] =
    3.17 +    layout.output_graph.iterator.collectFirst({
    3.18 +      case (Layout.Node(node), _) if Shapes.Node.shape(visualizer, node).contains(at) => node
    3.19 +    })
    3.20 +
    3.21 +  def find_dummy(at: Point2D): Option[Layout.Dummy] =
    3.22 +    layout.output_graph.iterator.collectFirst({
    3.23 +      case (dummy: Layout.Dummy, (d, _)) if Shapes.Dummy.shape(visualizer, d).contains(at) => dummy
    3.24 +    })
    3.25 +
    3.26    def bounding_box(): Rectangle2D.Double =
    3.27    {
    3.28      var x0 = 0.0