1/* Title: Pure/General/graphics_file.scala 2 Author: Makarius 3 4File system operations for Graphics2D output. 5*/ 6 7package isabelle 8 9 10import java.io.{FileOutputStream, BufferedOutputStream, File => JFile} 11import java.awt.Graphics2D 12import java.awt.geom.Rectangle2D 13import java.awt.image.BufferedImage 14import javax.imageio.ImageIO 15 16import org.jfree.chart.JFreeChart 17 18import com.lowagie.text.pdf.{PdfWriter, BaseFont, FontMapper, DefaultFontMapper} 19 20 21object Graphics_File 22{ 23 /* PNG */ 24 25 def write_png(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72) 26 { 27 val scale = dpi / 72.0f 28 val w = (width * scale).round 29 val h = (height * scale).round 30 31 val img = new BufferedImage(w, h, BufferedImage.TYPE_INT_ARGB) 32 val gfx = img.createGraphics 33 try { 34 gfx.scale(scale, scale) 35 paint(gfx) 36 ImageIO.write(img, "png", file) 37 } 38 finally { gfx.dispose } 39 } 40 41 42 /* PDF */ 43 44 private def font_mapper(): FontMapper = 45 { 46 val mapper = new DefaultFontMapper 47 for (entry <- Isabelle_Fonts.fonts()) { 48 val params = new DefaultFontMapper.BaseFontParameters(File.platform_path(entry.path)) 49 params.encoding = BaseFont.IDENTITY_H 50 params.embedded = true 51 params.ttfAfm = entry.bytes.array 52 mapper.putName(entry.name, params) 53 } 54 mapper 55 } 56 57 def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int) 58 { 59 import com.lowagie.text.{Document, Rectangle} 60 61 using(new BufferedOutputStream(new FileOutputStream(file)))(out => 62 { 63 val document = new Document() 64 try { 65 document.setPageSize(new Rectangle(width, height)) 66 val writer = PdfWriter.getInstance(document, out) 67 document.open() 68 69 val cb = writer.getDirectContent() 70 val tp = cb.createTemplate(width, height) 71 val gfx = tp.createGraphics(width, height, font_mapper()) 72 73 paint(gfx) 74 gfx.dispose 75 76 cb.addTemplate(tp, 1, 0, 0, 1, 0, 0) 77 } 78 finally { document.close() } 79 }) 80 } 81 82 83 /* JFreeChart */ 84 85 def paint_chart(gfx: Graphics2D, chart: JFreeChart, width: Int, height: Int): Unit = 86 chart.draw(gfx, new Rectangle2D.Double(0, 0, width, height)) 87 88 def write_chart_png(file: JFile, chart: JFreeChart, width: Int, height: Int): Unit = 89 write_png(file, paint_chart(_, chart, width, height), width, height) 90 91 def write_chart_pdf(file: JFile, chart: JFreeChart, width: Int, height: Int): Unit = 92 write_pdf(file, paint_chart(_, chart, width, height), width, height) 93} 94