# HG changeset patch
# User wenzelm
# Date 1397077460 -7200
# Node ID 5fda9e5c5874660120792f1aa1c969646e6bb606
# Parent  90f17a04567d01131cf0759be3359280a5cf1b80
basic URL operations (with Isabelle/Scala error handling);

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 }
+  }
+}
+
diff -r 90f17a04567d -r 5fda9e5c5874 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Apr 09 20:58:32 2014 +0200
+++ b/src/Pure/build-jars	Wed Apr 09 23:04:20 2014 +0200
@@ -31,6 +31,7 @@
   General/symbol.scala
   General/time.scala
   General/timing.scala
+  General/url.scala
   General/xz_file.scala
   GUI/color_value.scala
   GUI/gui.scala