1.1 --- a/src/Pure/General/graphics_file.scala	Thu Feb 14 15:27:10 2013 +0100
     1.2 +++ b/src/Pure/General/graphics_file.scala	Thu Feb 14 21:31:25 2013 +0100
     1.3 @@ -8,8 +8,11 @@
     1.4  
     1.5  
     1.6  import java.awt.Graphics2D
     1.7 +import java.awt.geom.Rectangle2D
     1.8  import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
     1.9  
    1.10 +import org.jfree.chart.JFreeChart
    1.11 +
    1.12  
    1.13  object Graphics_File
    1.14  {
    1.15 @@ -44,5 +47,14 @@
    1.16  
    1.17    def write_pdf(path: Path, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
    1.18      write_pdf(path.file, paint, width, height)
    1.19 +
    1.20 +  def write_pdf(file: JFile, chart: JFreeChart, width: Int, height: Int)
    1.21 +  {
    1.22 +    def paint(gfx: Graphics2D) = chart.draw(gfx, new Rectangle2D.Double(0, 0, width, height))
    1.23 +    write_pdf(file, paint _, width, height)
    1.24 +  }
    1.25 +
    1.26 +  def write_pdf(path: Path, chart: JFreeChart, width: Int, height: Int): Unit =
    1.27 +    write_pdf(path.file, chart, width, height)
    1.28  }
    1.29