equal
deleted
inserted
replaced
24 def paint(gfx: Graphics2D) |
24 def paint(gfx: Graphics2D) |
25 { |
25 { |
26 gfx.setColor(Color.WHITE) |
26 gfx.setColor(Color.WHITE) |
27 gfx.fillRect(0, 0, w, h) |
27 gfx.fillRect(0, 0, w, h) |
28 gfx.translate(- box.x, - box.y) |
28 gfx.translate(- box.x, - box.y) |
29 graphview.paint_all_visible(gfx) |
29 graphview.paint(gfx) |
30 } |
30 } |
31 |
31 |
32 val name = file.getName |
32 val name = file.getName |
33 if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) |
33 if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) |
34 else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h) |
34 else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h) |