# HG changeset patch
# User wenzelm
# Date 1678025957 -3600
# Node ID 6aae7486e94ae7fc3b4e9cbe6139657a28a8f48d
# Parent  acaa89cb977bf8bbc981550e889517319585cf3a
more operations;

diff -r acaa89cb977b -r 6aae7486e94a src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Sun Mar 05 14:53:32 2023 +0100
+++ b/src/Pure/ROOT.scala	Sun Mar 05 15:19:17 2023 +0100
@@ -9,7 +9,11 @@
   val error = Exn.error _
   def cat_error(msgs: String*): Nothing = Exn.cat_error(msgs:_*)
 
-  def using[A <: AutoCloseable, B](a: A)(f: A => B): B = Library.using(a)(f)
+  def using[A <: AutoCloseable, B](a: A)(f: A => B): B =
+    Library.using(a)(f)
+  def using_option[A <: AutoCloseable, B](opt: Option[A])(f: A => B): Option[B] =
+    Library.using_option(opt)(f)
+
   val space_explode = Library.space_explode _
   val split_lines = Library.split_lines _
   val cat_lines = Library.cat_lines _
@@ -22,4 +26,3 @@
   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
   def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
 }
-
diff -r acaa89cb977b -r 6aae7486e94a 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 */