src/Pure/library.scala

--- 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