src/Pure/library.scala

--- a/src/Pure/library.scala	Sun Mar 05 14:53:32 2023 +0100
+++ b/src/Pure/library.scala	Sun Mar 05 15:19:17 2023 +0100
@@ -20,6 +20,9 @@
     finally { if (a != null) a.close() }
   }
 
+  def using_option[A <: AutoCloseable, B](opt: Option[A])(f: A => B): Option[B] =
+    opt.map(a => using(a)(f))
+
 
   /* integers */