--- a/src/Pure/General/graphics_file.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/graphics_file.scala Fri Apr 01 23:19:12 2022 +0200
@@ -60,7 +60,7 @@
def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int): Unit = {
import com.lowagie.text.{Document, Rectangle}
- using(new BufferedOutputStream(new FileOutputStream(file)))(out => {
+ using(new BufferedOutputStream(new FileOutputStream(file))) { out =>
val document = new Document()
try {
document.setPageSize(new Rectangle(width.toFloat, height.toFloat))
@@ -77,7 +77,7 @@
cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
}
finally { document.close() }
- })
+ }
}