--- /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 }
+ }
+}
+
--- 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