# HG changeset patch
# User wenzelm
# Date 1411640532 -7200
# Node ID 9c3da105db2d46551093fea90fa4a90d9951324e
# Parent  5dbb09cc5a019c7f2dd956efd6519af1f778ee2e
support for PNG output;

diff -r 5dbb09cc5a01 -r 9c3da105db2d src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Thu Sep 25 10:36:39 2014 +0200
+++ b/src/Pure/General/graphics_file.scala	Thu Sep 25 12:22:12 2014 +0200
@@ -7,15 +7,36 @@
 package isabelle
 
 
+import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
 import java.awt.Graphics2D
 import java.awt.geom.Rectangle2D
-import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
+import java.awt.image.BufferedImage
+import javax.imageio.ImageIO
 
 import org.jfree.chart.JFreeChart
 
 
 object Graphics_File
 {
+  /* PNG */
+
+  def write_png(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72)
+  {
+    val scale = dpi / 72.0f
+    val w = (width * scale).round
+    val h = (height * scale).round
+
+    val img = new BufferedImage(w, h, BufferedImage.TYPE_INT_ARGB)
+    val gfx = img.createGraphics
+    try {
+      gfx.scale(scale, scale)
+      paint(gfx)
+      ImageIO.write(img, "png", file)
+    }
+    finally { gfx.dispose }
+  }
+
+
   /* PDF */
 
   def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)