src/Pure/General/graphics_file.scala
author wenzelm
Sat, 11 Dec 2021 11:24:48 +0100
changeset 74913 c2a2be496f35
parent 73343 d0378baf7d06
child 75393 87ebf5a50283
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/graphics_file.scala
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     3
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     4
File system operations for Graphics2D output.
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     5
*/
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     6
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     7
package isabelle
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     8
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
     9
58451
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    10
import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    11
import java.awt.Graphics2D
51127
5cf1604b9ef5 write_pdf for JFreeChart;
wenzelm
parents: 51098
diff changeset
    12
import java.awt.geom.Rectangle2D
58451
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    13
import java.awt.image.BufferedImage
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    14
import javax.imageio.ImageIO
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    15
51127
5cf1604b9ef5 write_pdf for JFreeChart;
wenzelm
parents: 51098
diff changeset
    16
import org.jfree.chart.JFreeChart
5cf1604b9ef5 write_pdf for JFreeChart;
wenzelm
parents: 51098
diff changeset
    17
61177
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    18
import com.lowagie.text.pdf.{PdfWriter, BaseFont, FontMapper, DefaultFontMapper}
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    19
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    20
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    21
object Graphics_File
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    22
{
58451
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    23
  /* PNG */
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    24
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 69393
diff changeset
    25
  def write_png(
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 69393
diff changeset
    26
    file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72): Unit =
58451
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    27
  {
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    28
    val scale = dpi / 72.0f
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    29
    val w = (width * scale).round
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    30
    val h = (height * scale).round
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    31
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    32
    val img = new BufferedImage(w, h, BufferedImage.TYPE_INT_ARGB)
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    33
    val gfx = img.createGraphics
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    34
    try {
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    35
      gfx.scale(scale, scale)
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    36
      paint(gfx)
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    37
      ImageIO.write(img, "png", file)
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    38
    }
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    39
    finally { gfx.dispose }
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    40
  }
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    41
9c3da105db2d support for PNG output;
wenzelm
parents: 51127
diff changeset
    42
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    43
  /* PDF */
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    44
61177
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    45
  private def font_mapper(): FontMapper =
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    46
  {
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    47
    val mapper = new DefaultFontMapper
69360
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69355
diff changeset
    48
    for (entry <- Isabelle_Fonts.fonts()) {
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69355
diff changeset
    49
      val params = new DefaultFontMapper.BaseFontParameters(File.platform_path(entry.path))
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69355
diff changeset
    50
      params.encoding = BaseFont.IDENTITY_H
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69355
diff changeset
    51
      params.embedded = true
69365
c5b3860d29ef avoid loading of font file, to eliminate "Illegal reflective access by com.lowagie.text.pdf.MappedRandomAccessFile$1 (iText-2.1.5.jar) to method java.nio.DirectByteBuffer.cleaner()" -- due to com.lowagie.text.pdf.TrueTypeFont.process() / RandomAccessFileOrArray;
wenzelm
parents: 69360
diff changeset
    52
      params.ttfAfm = entry.bytes.array
69360
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69355
diff changeset
    53
      mapper.putName(entry.name, params)
61177
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    54
    }
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    55
    mapper
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    56
  }
8e6a3fbc91fa provide FontMapper for embedded fonts;
wenzelm
parents: 58451
diff changeset
    57
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 69393
diff changeset
    58
  def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    59
  {
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    60
    import com.lowagie.text.{Document, Rectangle}
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    61
69393
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69365
diff changeset
    62
    using(new BufferedOutputStream(new FileOutputStream(file)))(out =>
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69365
diff changeset
    63
    {
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    64
      val document = new Document()
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    65
      try {
73343
d0378baf7d06 tuned --- avoid deprecated conversions between certain number type;
wenzelm
parents: 73340
diff changeset
    66
        document.setPageSize(new Rectangle(width.toFloat, height.toFloat))
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    67
        val writer = PdfWriter.getInstance(document, out)
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    68
        document.open()
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    69
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    70
        val cb = writer.getDirectContent()
73343
d0378baf7d06 tuned --- avoid deprecated conversions between certain number type;
wenzelm
parents: 73340
diff changeset
    71
        val tp = cb.createTemplate(width.toFloat, height.toFloat)
d0378baf7d06 tuned --- avoid deprecated conversions between certain number type;
wenzelm
parents: 73340
diff changeset
    72
        val gfx = tp.createGraphics(width.toFloat, height.toFloat, font_mapper())
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    73
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    74
        paint(gfx)
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    75
        gfx.dispose
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    76
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    77
        cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    78
      }
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    79
      finally { document.close() }
69393
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69365
diff changeset
    80
    })
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    81
  }
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    82
65862
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    83
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    84
  /* JFreeChart */
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    85
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    86
  def paint_chart(gfx: Graphics2D, chart: JFreeChart, width: Int, height: Int): Unit =
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    87
    chart.draw(gfx, new Rectangle2D.Double(0, 0, width, height))
51127
5cf1604b9ef5 write_pdf for JFreeChart;
wenzelm
parents: 51098
diff changeset
    88
65862
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    89
  def write_chart_png(file: JFile, chart: JFreeChart, width: Int, height: Int): Unit =
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    90
    write_png(file, paint_chart(_, chart, width, height), width, height)
51127
5cf1604b9ef5 write_pdf for JFreeChart;
wenzelm
parents: 51098
diff changeset
    91
65862
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    92
  def write_chart_pdf(file: JFile, chart: JFreeChart, width: Int, height: Int): Unit =
5441c51a2d38 more JFreeChart operations;
wenzelm
parents: 65086
diff changeset
    93
    write_pdf(file, paint_chart(_, chart, width, height), width, height)
51098
22d5c010ef5c file system operations for Graphics2D output;
wenzelm
parents:
diff changeset
    94
}