1/*  Title:      Tools/Graphview/graph_file.scala
2    Author:     Makarius
3
4File system operations for graph output.
5*/
6
7package isabelle.graphview
8
9
10import isabelle._
11
12import java.io.{File => JFile}
13import java.awt.{Color, Graphics2D}
14
15
16object 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}
48