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 _