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