src/Pure/ROOT.scala
changeset 63789 af28929ff219
parent 62845 31177a9c3025
child 64173 85ff21510ba9
--- 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 _