src/Pure/library.scala

--- a/src/Pure/library.scala	Fri Jun 23 13:51:23 2023 +0200
+++ b/src/Pure/library.scala	Fri Jun 23 14:43:15 2023 +0200
@@ -23,6 +23,16 @@
   def using_option[A <: AutoCloseable, B](opt: Option[A])(f: A => B): Option[B] =
     opt.map(a => using(a)(f))
 
+  def using_optional[A <: AutoCloseable, B](opt: Option[A])(f: Option[A] => B): B = {
+    try { f(opt) }
+    finally {
+      opt match {
+        case Some(a) if a != null => a.close()
+        case _ =>
+      }
+    }
+  }
+
 
   /* integers */