author | wenzelm |
Fri, 17 Mar 2017 20:33:27 +0100 | |
changeset 65292 | e3bd1e7ddd23 |
parent 65188 | 50cfc6775361 |
child 66234 | 836898197296 |
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} |
65188 | 11 |
import java.nio.file.{Paths, FileSystemNotFoundException} |
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 = |
65069 | 40 |
using(url.openStream)(stream => |
41 |
File.read_stream(if (gzip) new GZIPInputStream(stream) else stream)) |
|
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) |
|
64729 | 48 |
|
49 |
||
50 |
/* file URIs */ |
|
51 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
52 |
def print_file(file: JFile): String = file.toPath.toAbsolutePath.toUri.normalize.toString |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
53 |
def print_file_name(name: String): String = print_file(new JFile(name)) |
64775 | 54 |
|
55 |
def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile |
|
64729 | 56 |
|
57 |
def is_wellformed_file(uri: String): Boolean = |
|
64775 | 58 |
try { parse_file(uri); true } |
65188 | 59 |
catch { |
60 |
case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException => |
|
61 |
false |
|
62 |
} |
|
64730 | 63 |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
64 |
def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile |
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
65 |
def canonical_file_name(uri: String): String = canonical_file(uri).getPath |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
66 |
} |