# HG changeset patch
# User wenzelm
# Date 1360758698 -3600
# Node ID 22d5c010ef5c9c3f79cf66a7cb3acdd84c0df828
# Parent  72c355842f42252fcc95e59f4565adcde9a431a5
file system operations for Graphics2D output;

diff -r 72c355842f42 -r 22d5c010ef5c src/Pure/General/graphics_file.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/graphics_file.scala	Wed Feb 13 13:31:38 2013 +0100
@@ -0,0 +1,48 @@
+/*  Title:      Pure/General/graphics_file.scala
+    Author:     Makarius
+
+File system operations for Graphics2D output.
+*/
+
+package isabelle
+
+
+import java.awt.Graphics2D
+import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
+
+
+object Graphics_File
+{
+  /* PDF */
+
+  def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)
+  {
+    import com.lowagie.text.{Document, Rectangle}
+    import com.lowagie.text.pdf.PdfWriter
+
+    val out = new BufferedOutputStream(new FileOutputStream(file))
+    try {
+      val document = new Document()
+      try {
+        document.setPageSize(new Rectangle(width, height))
+        val writer = PdfWriter.getInstance(document, out)
+        document.open()
+
+        val cb = writer.getDirectContent()
+        val tp = cb.createTemplate(width, height)
+        val gfx = tp.createGraphics(width, height)
+
+        paint(gfx)
+        gfx.dispose
+
+        cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
+      }
+      finally { document.close() }
+    }
+    finally { out.close }
+  }
+
+  def write_pdf(path: Path, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
+    write_pdf(path.file, paint, width, height)
+}
+
diff -r 72c355842f42 -r 22d5c010ef5c src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Feb 13 12:42:59 2013 +0100
+++ b/src/Pure/build-jars	Wed Feb 13 13:31:38 2013 +0100
@@ -16,6 +16,7 @@
   General/exn.scala
   General/file.scala
   General/graph.scala
+  General/graphics_file.scala
   General/linear_set.scala
   General/path.scala
   General/position.scala