src/Tools/Graphview/visualizer.scala
changeset 59303 15cd9bcd6ddb
parent 59302 4d985afc0565
child 59305 b5e33012180e
     1.1 --- a/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:33:30 2015 +0100
     1.2 +++ b/src/Tools/Graphview/visualizer.scala	Tue Jan 06 16:41:31 2015 +0100
     1.3 @@ -23,22 +23,14 @@
     1.4    /* layout state */
     1.5  
     1.6    // owned by GUI thread
     1.7 -  private var layout: Layout = Layout.empty
     1.8 +  private var _layout: Layout = Layout.empty
     1.9 +  def layout: Layout = _layout
    1.10  
    1.11    def metrics: Metrics = layout.metrics
    1.12    def visible_graph: Graph_Display.Graph = layout.input_graph
    1.13  
    1.14 -  def get_vertex(v: Layout.Vertex): Layout.Point = layout.get_vertex(v)
    1.15 -  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double)
    1.16 -  {
    1.17 -    layout = layout.translate_vertex(v, dx, dy)
    1.18 -  }
    1.19 -
    1.20 -  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
    1.21 -    layout.dummies_iterator(edge)
    1.22 -
    1.23 -  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
    1.24 -    layout.find_dummy(pred)
    1.25 +  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
    1.26 +    _layout = _layout.translate_vertex(v, dx, dy)
    1.27  
    1.28    def bounding_box(): Rectangle2D.Double =
    1.29    {
    1.30 @@ -68,7 +60,7 @@
    1.31      val visible_graph = model.make_visible_graph()
    1.32  
    1.33      // FIXME avoid expensive operation on GUI thread
    1.34 -    layout = Layout.make(metrics, visible_graph)
    1.35 +    _layout = Layout.make(metrics, visible_graph)
    1.36    }
    1.37  
    1.38