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