tuned signature;
authorwenzelm
Tue Jan 06 16:41:31 2015 +0100 (2015-01-06)
changeset 5930315cd9bcd6ddb
parent 59302 4d985afc0565
child 59304 848e27e4ac37
tuned signature;
src/Tools/Graphview/graph_panel.scala
src/Tools/Graphview/shapes.scala
src/Tools/Graphview/visualizer.scala
     1.1 --- a/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:33:30 2015 +0100
     1.2 +++ b/src/Tools/Graphview/graph_panel.scala	Tue Jan 06 16:41:31 2015 +0100
     1.3 @@ -176,7 +176,7 @@
     1.4      }
     1.5  
     1.6      def dummy(at: Point2D): Option[Layout.Dummy] =
     1.7 -      visualizer.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
     1.8 +      visualizer.layout.find_dummy(d => Shapes.Dummy.shape(visualizer, d).contains(at))
     1.9  
    1.10      def pressed(at: Point)
    1.11      {
     2.1 --- a/src/Tools/Graphview/shapes.scala	Tue Jan 06 16:33:30 2015 +0100
     2.2 +++ b/src/Tools/Graphview/shapes.scala	Tue Jan 06 16:41:31 2015 +0100
     2.3 @@ -24,7 +24,7 @@
     2.4      def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double =
     2.5      {
     2.6        val metrics = visualizer.metrics
     2.7 -      val p = visualizer.get_vertex(Layout.Node(node))
     2.8 +      val p = visualizer.layout.get_vertex(Layout.Node(node))
     2.9        val bounds = metrics.string_bounds(node.toString)
    2.10        val w2 = ((bounds.getWidth + metrics.pad_x) / 2).ceil
    2.11        val h2 = ((bounds.getHeight + metrics.pad_y) / 2).ceil
    2.12 @@ -74,13 +74,13 @@
    2.13    {
    2.14      def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
    2.15      {
    2.16 -      val p = visualizer.get_vertex(Layout.Node(edge._1))
    2.17 -      val q = visualizer.get_vertex(Layout.Node(edge._2))
    2.18 +      val p = visualizer.layout.get_vertex(Layout.Node(edge._1))
    2.19 +      val q = visualizer.layout.get_vertex(Layout.Node(edge._2))
    2.20        val ds =
    2.21        {
    2.22          val a = p.y min q.y
    2.23          val b = p.y max q.y
    2.24 -        visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
    2.25 +        visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
    2.26        }
    2.27        val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
    2.28  
    2.29 @@ -106,13 +106,13 @@
    2.30  
    2.31      def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
    2.32      {
    2.33 -      val p = visualizer.get_vertex(Layout.Node(edge._1))
    2.34 -      val q = visualizer.get_vertex(Layout.Node(edge._2))
    2.35 +      val p = visualizer.layout.get_vertex(Layout.Node(edge._1))
    2.36 +      val q = visualizer.layout.get_vertex(Layout.Node(edge._2))
    2.37        val ds =
    2.38        {
    2.39          val a = p.y min q.y
    2.40          val b = p.y max q.y
    2.41 -        visualizer.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
    2.42 +        visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
    2.43        }
    2.44  
    2.45        if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
     3.1 --- a/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:33:30 2015 +0100
     3.2 +++ b/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:41:31 2015 +0100
     3.3 @@ -23,22 +23,14 @@
     3.4    /* layout state */
     3.5  
     3.6    // owned by GUI thread
     3.7 -  private var layout: Layout = Layout.empty
     3.8 +  private var _layout: Layout = Layout.empty
     3.9 +  def layout: Layout = _layout
    3.10  
    3.11    def metrics: Metrics = layout.metrics
    3.12    def visible_graph: Graph_Display.Graph = layout.input_graph
    3.13  
    3.14 -  def get_vertex(v: Layout.Vertex): Layout.Point = layout.get_vertex(v)
    3.15 -  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double)
    3.16 -  {
    3.17 -    layout = layout.translate_vertex(v, dx, dy)
    3.18 -  }
    3.19 -
    3.20 -  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
    3.21 -    layout.dummies_iterator(edge)
    3.22 -
    3.23 -  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
    3.24 -    layout.find_dummy(pred)
    3.25 +  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
    3.26 +    _layout = _layout.translate_vertex(v, dx, dy)
    3.27  
    3.28    def bounding_box(): Rectangle2D.Double =
    3.29    {
    3.30 @@ -68,7 +60,7 @@
    3.31      val visible_graph = model.make_visible_graph()
    3.32  
    3.33      // FIXME avoid expensive operation on GUI thread
    3.34 -    layout = Layout.make(metrics, visible_graph)
    3.35 +    _layout = Layout.make(metrics, visible_graph)
    3.36    }
    3.37  
    3.38