src/Pure/General/graphics_file.scala
changeset 75394 42267c650205
parent 75393 87ebf5a50283
child 80368 9db395953106
--- 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() }
-    })
+    }
   }