# 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