src/Pure/General/url.scala
author wenzelm
Mon, 18 Aug 2014 12:17:31 +0200
changeset 57978 8f4a332500e4
parent 56503 9e23fafe4037
child 62248 dca0bac351b2
permissions -rw-r--r--
Added tag Isabelle2014-RC4 for changeset 113b43b84412

/*  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) }
    finally { stream.close }
  }
}