src/Pure/General/url.scala
author wenzelm
Thu, 10 Apr 2014 10:06:54 +0200
changeset 56503 9e23fafe4037
parent 56501 5fda9e5c5874
child 62248 dca0bac351b2
permissions -rw-r--r--
no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56501
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/url.scala
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     3
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     4
Basic URL operations.
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     5
*/
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     6
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     7
package isabelle
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     8
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
     9
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    10
import java.net.{URL, MalformedURLException}
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    11
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    12
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    13
object Url
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    14
{
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    15
  def apply(name: String): URL =
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    16
  {
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    17
    try { new URL(name) }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    18
    catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    19
  }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    20
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    21
  def is_wellformed(name: String): Boolean =
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    22
    try { Url(name); true }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    23
    catch { case ERROR(_) => false }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    24
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    25
  def is_readable(name: String): Boolean =
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    26
    try { Url(name).openStream.close; true }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    27
    catch { case ERROR(_) => false }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    28
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    29
  def read(name: String): String =
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    30
  {
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    31
    val stream = Url(name).openStream
56503
9e23fafe4037 no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;
wenzelm
parents: 56501
diff changeset
    32
    try { File.read_stream(stream) }
56501
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    33
    finally { stream.close }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    34
  }
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    35
}
5fda9e5c5874 basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff changeset
    36