author | wenzelm |
Thu, 12 May 2016 10:57:09 +0200 | |
changeset 63086 | 5c8e6a751adc |
parent 62248 | dca0bac351b2 |
child 63642 | d83a1eeff9d2 |
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} |
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 |
{ |
62248 | 15 |
def escape(name: String): String = |
16 |
(for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString |
|
17 |
||
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
18 |
def apply(name: String): URL = |
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 |
try { new URL(name) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
21 |
catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
22 |
} |
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 |
def is_wellformed(name: String): Boolean = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
25 |
try { Url(name); true } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
26 |
catch { case ERROR(_) => false } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
27 |
|
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
28 |
def is_readable(name: String): Boolean = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
29 |
try { Url(name).openStream.close; true } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
30 |
catch { case ERROR(_) => false } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
31 |
|
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
32 |
def read(name: String): String = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
33 |
{ |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
34 |
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
|
35 |
try { File.read_stream(stream) } |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
36 |
finally { stream.close } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
37 |
} |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
38 |
} |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
39 |