src/Tools/Graphview/shapes.scala
changeset 59291 506660c6792f
parent 59290 569a8109eeb2
child 59292 fef652c88263
equal deleted inserted replaced
59290:569a8109eeb2 59291:506660c6792f
    53     }
    53     }
    54   }
    54   }
    55 
    55 
    56   object Dummy
    56   object Dummy
    57   {
    57   {
    58     private val identity = new AffineTransform()
    58     def shape(visualizer: Visualizer, d: Layout.Point): Shape =
    59 
    59     {
    60     def shape(visualizer: Visualizer): Shape =
    60       val metrics = visualizer.metrics
    61     {
    61       val w = metrics.space_width
    62       val m = visualizer.metrics
    62       new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil)
    63       val w = (m.space_width / 2).ceil
    63     }
    64       new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
    64 
    65     }
    65     def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point)
    66 
       
    67     def paint(gfx: Graphics2D, visualizer: Visualizer): Unit =
       
    68       paint_transformed(gfx, visualizer, identity)
       
    69 
       
    70     def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform)
       
    71     {
    66     {
    72       gfx.setStroke(default_stroke)
    67       gfx.setStroke(default_stroke)
    73       gfx.setColor(visualizer.dummy_color)
    68       gfx.setColor(visualizer.dummy_color)
    74       gfx.draw(at.createTransformedShape(shape(visualizer)))
    69       gfx.draw(shape(visualizer, d))
    75     }
    70     }
    76   }
    71   }
    77 
    72 
    78   object Straight_Edge
    73   object Straight_Edge
    79   {
    74   {
    92 
    87 
    93       path.moveTo(p.x, p.y)
    88       path.moveTo(p.x, p.y)
    94       ds.foreach(d => path.lineTo(d.x, d.y))
    89       ds.foreach(d => path.lineTo(d.x, d.y))
    95       path.lineTo(q.x, q.y)
    90       path.lineTo(q.x, q.y)
    96 
    91 
    97       if (dummies)
    92       if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
    98         ds.foreach(d =>
       
    99           Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
       
   100 
    93 
   101       gfx.setStroke(default_stroke)
    94       gfx.setStroke(default_stroke)
   102       gfx.setColor(visualizer.edge_color(edge))
    95       gfx.setColor(visualizer.edge_color(edge))
   103       gfx.draw(path)
    96       gfx.draw(path)
   104 
    97 
   105       if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2))
    98       if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
   106     }
    99     }
   107   }
   100   }
   108 
   101 
   109   object Cardinal_Spline_Edge
   102   object Cardinal_Spline_Edge
   110   {
   103   {
   147         path.curveTo(
   140         path.curveTo(
   148           l.x + slack * dx2, l.y + slack * dy2,
   141           l.x + slack * dx2, l.y + slack * dy2,
   149           q.x - slack * dx2, q.y - slack * dy2,
   142           q.x - slack * dx2, q.y - slack * dy2,
   150           q.x, q.y)
   143           q.x, q.y)
   151 
   144 
   152         if (dummies)
   145         if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
   153           ds.foreach(d =>
       
   154             Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
       
   155 
   146 
   156         gfx.setStroke(default_stroke)
   147         gfx.setStroke(default_stroke)
   157         gfx.setColor(visualizer.edge_color(edge))
   148         gfx.setColor(visualizer.edge_color(edge))
   158         gfx.draw(path)
   149         gfx.draw(path)
   159 
   150 
   160         if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2))
   151         if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
   161       }
   152       }
   162     }
   153     }
   163   }
   154   }
   164 
   155 
   165   object Arrow_Head
   156   object Arrow_Head