src/Tools/Graphview/graph_file.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 61176 9791f631c20d
permissions -rw-r--r--
tuned imports;
     1 /*  Title:      Tools/Graphview/graph_file.scala
     2     Author:     Makarius
     3 
     4 File system operations for graph output.
     5 */
     6 
     7 package isabelle.graphview
     8 
     9 
    10 import isabelle._
    11 
    12 import java.io.{File => JFile}
    13 import java.awt.{Color, Graphics2D}
    14 
    15 
    16 object Graph_File
    17 {
    18   def write(file: JFile, graphview: Graphview)
    19   {
    20     val box = graphview.bounding_box()
    21     val w = box.width.ceil.toInt
    22     val h = box.height.ceil.toInt
    23 
    24     def paint(gfx: Graphics2D)
    25     {
    26       gfx.setColor(graphview.background_color)
    27       gfx.fillRect(0, 0, w, h)
    28       gfx.translate(- box.x, - box.y)
    29       graphview.paint(gfx)
    30     }
    31 
    32     val name = file.getName
    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)
    35     else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
    36   }
    37 
    38   def write(options: Options, file: JFile, graph: Graph_Display.Graph)
    39   {
    40     val the_options = options
    41     val graphview =
    42       new Graphview(graph.transitive_reduction_acyclic) { def options = the_options }
    43     graphview.update_layout()
    44 
    45     write(file, graphview)
    46   }
    47 }