# HG changeset patch
# User wenzelm
# Date 1360873885 -3600
# Node ID 5cf1604b9ef550ecc2872f6551097b66e7240d1d
# Parent  df86080de4cbe098d556686afa3a072ff60f15d4
write_pdf for JFreeChart;

diff -r df86080de4cb -r 5cf1604b9ef5 src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Thu Feb 14 15:27:10 2013 +0100
+++ b/src/Pure/General/graphics_file.scala	Thu Feb 14 21:31:25 2013 +0100
@@ -8,8 +8,11 @@
 
 
 import java.awt.Graphics2D
+import java.awt.geom.Rectangle2D
 import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
 
+import org.jfree.chart.JFreeChart
+
 
 object Graphics_File
 {
@@ -44,5 +47,14 @@
 
   def write_pdf(path: Path, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
     write_pdf(path.file, paint, width, height)
+
+  def write_pdf(file: JFile, chart: JFreeChart, width: Int, height: Int)
+  {
+    def paint(gfx: Graphics2D) = chart.draw(gfx, new Rectangle2D.Double(0, 0, width, height))
+    write_pdf(file, paint _, width, height)
+  }
+
+  def write_pdf(path: Path, chart: JFreeChart, width: Int, height: Int): Unit =
+    write_pdf(path.file, chart, width, height)
 }