author | wenzelm |
Tue, 09 Aug 2016 23:19:35 +0200 | |
changeset 63645 | d7e0004d4321 |
parent 63642 | d83a1eeff9d2 |
child 64729 | 4eccd9bc5fd9 |
permissions | -rw-r--r-- |
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} |
63642 | 11 |
import java.util.zip.GZIPInputStream |
56501
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 |
|
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
14 |
object Url |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
15 |
{ |
62248 | 16 |
def escape(name: String): String = |
17 |
(for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString |
|
18 |
||
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
19 |
def apply(name: String): URL = |
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 |
try { new URL(name) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
22 |
catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
23 |
} |
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_wellformed(name: String): Boolean = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
26 |
try { Url(name); 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 is_readable(name: String): Boolean = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
30 |
try { Url(name).openStream.close; true } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
31 |
catch { case ERROR(_) => false } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
32 |
|
63642 | 33 |
|
34 |
/* read */ |
|
35 |
||
63645 | 36 |
private def read(url: URL, gzip: Boolean): String = |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
37 |
{ |
63645 | 38 |
val stream = url.openStream |
63642 | 39 |
try { File.read_stream(if (gzip) new GZIPInputStream(stream) else stream) } |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
40 |
finally { stream.close } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
41 |
} |
63642 | 42 |
|
63645 | 43 |
def read(url: URL): String = read(url, false) |
44 |
def read_gzip(url: URL): String = read(url, true) |
|
45 |
||
46 |
def read(name: String): String = read(Url(name), false) |
|
47 |
def read_gzip(name: String): String = read(Url(name), true) |
|
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
48 |
} |