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