author | wenzelm |
Wed, 04 Jan 2017 12:03:45 +0100 | |
changeset 64775 | dd3797f1e0d6 |
parent 64766 | 6fd05caf55f0 |
child 64777 | ca09695eb43c |
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 |
|
64729 | 10 |
import java.io.{File => JFile} |
64775 | 11 |
import java.nio.file.Paths |
64729 | 12 |
import java.net.{URI, URISyntaxException} |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
13 |
import java.net.{URL, MalformedURLException} |
63642 | 14 |
import java.util.zip.GZIPInputStream |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
15 |
|
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 |
object Url |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
18 |
{ |
62248 | 19 |
def escape(name: String): String = |
20 |
(for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString |
|
21 |
||
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
22 |
def apply(name: String): URL = |
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 |
try { new URL(name) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
25 |
catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
26 |
} |
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_wellformed(name: String): Boolean = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
29 |
try { Url(name); 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 is_readable(name: String): Boolean = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
33 |
try { Url(name).openStream.close; true } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
34 |
catch { case ERROR(_) => false } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
35 |
|
63642 | 36 |
|
37 |
/* read */ |
|
38 |
||
63645 | 39 |
private def read(url: URL, gzip: Boolean): String = |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
40 |
{ |
63645 | 41 |
val stream = url.openStream |
63642 | 42 |
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
|
43 |
finally { stream.close } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
44 |
} |
63642 | 45 |
|
63645 | 46 |
def read(url: URL): String = read(url, false) |
47 |
def read_gzip(url: URL): String = read(url, true) |
|
48 |
||
49 |
def read(name: String): String = read(Url(name), false) |
|
50 |
def read_gzip(name: String): String = read(Url(name), true) |
|
64729 | 51 |
|
52 |
||
53 |
/* file URIs */ |
|
54 |
||
64775 | 55 |
def print_file(file: JFile): String = |
56 |
file.toPath.toAbsolutePath.toUri.normalize.toString |
|
57 |
||
58 |
def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile |
|
64729 | 59 |
|
60 |
def is_wellformed_file(uri: String): Boolean = |
|
64775 | 61 |
try { parse_file(uri); true } |
64729 | 62 |
catch { case _: URISyntaxException | _: IllegalArgumentException => false } |
64730 | 63 |
|
64759 | 64 |
def normalize_file(uri: String): String = |
64775 | 65 |
if (is_wellformed_file(uri)) print_file(parse_file(uri)) else uri |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
66 |
} |