src/Tools/Graphview/graphview.scala
changeset 59460 3a357fef24e8
parent 59459 985fc55e9f27
child 59462 c7eff4356885
equal deleted inserted replaced
59459:985fc55e9f27 59460:3a357fef24e8
   133       curr = (curr + 1) % filter_colors.length
   133       curr = (curr + 1) % filter_colors.length
   134       filter_colors(curr)
   134       filter_colors(curr)
   135     }
   135     }
   136   }
   136   }
   137 
   137 
   138   def paint_all_visible(gfx: Graphics2D)
   138   def paint(gfx: Graphics2D)
   139   {
   139   {
   140     gfx.setRenderingHints(Metrics.rendering_hints)
   140     gfx.setRenderingHints(Metrics.rendering_hints)
   141 
   141 
   142     for (node <- graphview.current_node)
   142     for (node <- graphview.current_node)
   143       Shapes.highlight_node(gfx, graphview, node)
   143       Shapes.highlight_node(gfx, graphview, node)