13 import java.awt.{Color, Graphics2D} |
13 import java.awt.{Color, Graphics2D} |
14 |
14 |
15 |
15 |
16 object Graph_File |
16 object Graph_File |
17 { |
17 { |
18 def write(file: JFile, visualizer: Visualizer) |
18 def write(file: JFile, graphview: Graphview) |
19 { |
19 { |
20 val box = visualizer.bounding_box() |
20 val box = graphview.bounding_box() |
21 val w = box.width.ceil.toInt |
21 val w = box.width.ceil.toInt |
22 val h = box.height.ceil.toInt |
22 val h = box.height.ceil.toInt |
23 |
23 |
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 visualizer.paint_all_visible(gfx) |
29 graphview.paint_all_visible(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) |
38 def write(options: Options, file: JFile, graph: Graph_Display.Graph) |
38 def write(options: Options, file: JFile, graph: Graph_Display.Graph) |
39 { |
39 { |
40 val model = new Model(graph.transitive_reduction_acyclic) |
40 val model = new Model(graph.transitive_reduction_acyclic) |
41 |
41 |
42 val the_options = options |
42 val the_options = options |
43 val visualizer = new Visualizer(model) { def options = the_options } |
43 val graphview = new Graphview(model) { def options = the_options } |
44 visualizer.update_layout() |
44 graphview.update_layout() |
45 |
45 |
46 write(file, visualizer) |
46 write(file, graphview) |
47 } |
47 } |
48 } |
48 } |