diff -r 90f17a04567d -r 5fda9e5c5874 src/Pure/General/url.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/url.scala	Wed Apr 09 23:04:20 2014 +0200
@@ -0,0 +1,36 @@
+/*  Title:      Pure/General/url.scala
+    Author:     Makarius
+
+Basic URL operations.
+*/
+
+package isabelle
+
+
+import java.net.{URL, MalformedURLException}
+
+
+object Url
+{
+  def apply(name: String): URL =
+  {
+    try { new URL(name) }
+    catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
+  }
+
+  def is_wellformed(name: String): Boolean =
+    try { Url(name); true }
+    catch { case ERROR(_) => false }
+
+  def is_readable(name: String): Boolean =
+    try { Url(name).openStream.close; true }
+    catch { case ERROR(_) => false }
+
+  def read(name: String): String =
+  {
+    val stream = Url(name).openStream
+    try { File.read_stream(stream) }  // FIXME proper text encoding!?
+    finally { stream.close }
+  }
+}
+