src/Tools/Graphview/graph_file.scala
changeset 59459 985fc55e9f27
parent 59443 5b552b4f63a5
child 59460 3a357fef24e8
equal deleted inserted replaced
59458:9de8ac92cafa 59459:985fc55e9f27
    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 }