--- a/src/Pure/ROOT.scala Mon Sep 05 10:34:45 2016 +0200
+++ b/src/Pure/ROOT.scala Mon Sep 05 11:43:37 2016 +0200
@@ -11,6 +11,7 @@
val error = Exn.error _
val cat_error = Exn.cat_error _
+ def using[A <: { def close() }, B](x: A)(f: A => B): B = Library.using(x)(f)
val space_explode = Library.space_explode _
val split_lines = Library.split_lines _
val cat_lines = Library.cat_lines _
--- a/src/Pure/library.scala Mon Sep 05 10:34:45 2016 +0200
+++ b/src/Pure/library.scala Mon Sep 05 11:43:37 2016 +0200
@@ -15,6 +15,15 @@
object Library
{
+ /* resource management */
+
+ def using[A <: { def close() }, B](x: A)(f: A => B): B =
+ {
+ try { f(x) }
+ finally { if (x != null) x.close() }
+ }
+
+
/* integers */
private val small_int = 10000