author | wenzelm |
Sat, 04 Sep 2021 21:25:08 +0200 | |
changeset 74232 | 1091880266e5 |
parent 73417 | 1dcc2b228b8b |
child 75393 | 87ebf5a50283 |
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} |
67245 | 12 |
import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder} |
69901 | 13 |
import java.util.Locale |
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 |
{ |
69901 | 19 |
/* special characters */ |
20 |
||
21 |
def escape_special(c: Char): String = |
|
71163 | 22 |
if ("!#$&'()*+,/:;=?@[]".contains(c)) { |
23 |
String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt)) |
|
24 |
} |
|
69901 | 25 |
else c.toString |
26 |
||
71601 | 27 |
def escape_special(s: String): String = s.iterator.map(escape_special).mkString |
69901 | 28 |
|
29 |
def escape_name(name: String): String = |
|
30 |
name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString |
|
31 |
||
32 |
||
33 |
/* make and check URLs */ |
|
62248 | 34 |
|
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
35 |
def apply(name: String): URL = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
36 |
{ |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
37 |
try { new URL(name) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
38 |
catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
39 |
} |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
40 |
|
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
41 |
def is_wellformed(name: String): Boolean = |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
42 |
try { Url(name); true } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
43 |
catch { case ERROR(_) => false } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
44 |
|
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
45 |
def is_readable(name: String): Boolean = |
73367 | 46 |
try { Url(name).openStream.close(); true } |
56501
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
47 |
catch { case ERROR(_) => false } |
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
wenzelm
parents:
diff
changeset
|
48 |
|
63642 | 49 |
|
73417 | 50 |
/* file name */ |
51 |
||
52 |
def file_name(url: URL): String = |
|
53 |
Library.take_suffix[Char](c => c != '/' && c != '\\', url.getFile.toString.toList)._2.mkString |
|
72558 | 54 |
|
55 |
def trim_index(url: URL): URL = |
|
56 |
{ |
|
57 |
Library.try_unprefix("/index.html", url.toString) match { |
|
58 |
case Some(u) => Url(u) |
|
59 |
case None => |
|
60 |
Library.try_unprefix("/index.php", url.toString) match { |
|
61 |
case Some(u) => Url(u) |
|
62 |
case None => url |
|
63 |
} |
|
64 |
} |
|
65 |
} |
|
66 |
||
67 |
||
67245 | 68 |
/* strings */ |
69 |
||
70 |
def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name) |
|
71 |
def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name) |
|
72 |
||
73 |
||
63642 | 74 |
/* read */ |
75 |
||
63645 | 76 |
private def read(url: URL, gzip: Boolean): String = |
65069 | 77 |
using(url.openStream)(stream => |
78 |
File.read_stream(if (gzip) new GZIPInputStream(stream) else stream)) |
|
63642 | 79 |
|
63645 | 80 |
def read(url: URL): String = read(url, false) |
81 |
def read_gzip(url: URL): String = read(url, true) |
|
82 |
||
83 |
def read(name: String): String = read(Url(name), false) |
|
84 |
def read_gzip(name: String): String = read(Url(name), true) |
|
64729 | 85 |
|
86 |
||
87 |
/* file URIs */ |
|
88 |
||
66234 | 89 |
def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
90 |
def print_file_name(name: String): String = print_file(new JFile(name)) |
64775 | 91 |
|
92 |
def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile |
|
64729 | 93 |
|
94 |
def is_wellformed_file(uri: String): Boolean = |
|
64775 | 95 |
try { parse_file(uri); true } |
65188 | 96 |
catch { |
97 |
case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException => |
|
98 |
false |
|
99 |
} |
|
64730 | 100 |
|
66235
d4fa51e7c4ff
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
wenzelm
parents:
66234
diff
changeset
|
101 |
def absolute_file(uri: String): JFile = File.absolute(parse_file(uri)) |
d4fa51e7c4ff
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
wenzelm
parents:
66234
diff
changeset
|
102 |
def absolute_file_name(uri: String): String = absolute_file(uri).getPath |
d4fa51e7c4ff
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
wenzelm
parents:
66234
diff
changeset
|
103 |
|
66234 | 104 |
def canonical_file(uri: String): JFile = File.canonical(parse_file(uri)) |
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
105 |
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
|
106 |
} |