# HG changeset patch
# User wenzelm
# Date 1473068617 -7200
# Node ID af28929ff219fa70c86cd5756faf6581b58b561c
# Parent  3160826b92f889b271c523e3966898aad4ce6ff8
support resource management;

diff -r 3160826b92f8 -r af28929ff219 src/Pure/ROOT.scala
--- 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 _
diff -r 3160826b92f8 -r af28929ff219 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