--- a/src/Pure/General/graphics_file.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/graphics_file.scala Mon Mar 01 22:22:12 2021 +0100
@@ -22,7 +22,8 @@
{
/* PNG */
- def write_png(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72)
+ def write_png(
+ file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72): Unit =
{
val scale = dpi / 72.0f
val w = (width * scale).round
@@ -54,7 +55,7 @@
mapper
}
- def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)
+ def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
{
import com.lowagie.text.{Document, Rectangle}