1/*  Title:      Pure/General/url.scala
2    Author:     Makarius
3
4Basic URL operations.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11import java.nio.file.{Paths, FileSystemNotFoundException}
12import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
13import java.util.Locale
14import java.util.zip.GZIPInputStream
15
16
17object Url
18{
19  /* special characters */
20
21  def escape_special(c: Char): String =
22    if ("!#$&'()*+,/:;=?@[]".contains(c)) {
23      String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt))
24    }
25    else c.toString
26
27  def escape_special(s: String): String = s.iterator.map(escape_special(_)).mkString
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 */
34
35  def apply(name: String): URL =
36  {
37    try { new URL(name) }
38    catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
39  }
40
41  def is_wellformed(name: String): Boolean =
42    try { Url(name); true }
43    catch { case ERROR(_) => false }
44
45  def is_readable(name: String): Boolean =
46    try { Url(name).openStream.close; true }
47    catch { case ERROR(_) => false }
48
49
50  /* strings */
51
52  def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
53  def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
54
55
56  /* read */
57
58  private def read(url: URL, gzip: Boolean): String =
59    using(url.openStream)(stream =>
60      File.read_stream(if (gzip) new GZIPInputStream(stream) else stream))
61
62  def read(url: URL): String = read(url, false)
63  def read_gzip(url: URL): String = read(url, true)
64
65  def read(name: String): String = read(Url(name), false)
66  def read_gzip(name: String): String = read(Url(name), true)
67
68  def read_bytes(url: URL): Bytes =
69  {
70    val connection = url.openConnection
71    val length = connection.getContentLength
72    using(connection.getInputStream)(Bytes.read_stream(_, hint = length))
73  }
74
75
76  /* file URIs */
77
78  def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
79  def print_file_name(name: String): String = print_file(new JFile(name))
80
81  def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
82
83  def is_wellformed_file(uri: String): Boolean =
84    try { parse_file(uri); true }
85    catch {
86      case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException =>
87        false
88    }
89
90  def absolute_file(uri: String): JFile = File.absolute(parse_file(uri))
91  def absolute_file_name(uri: String): String = absolute_file(uri).getPath
92
93  def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
94  def canonical_file_name(uri: String): String = canonical_file(uri).getPath
95}
96