--- 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)
}