src/Pure/General/url.scala
author wenzelm
Sat, 11 Mar 2017 20:18:06 +0100
changeset 65188 50cfc6775361
parent 65069 1995b421d8ef
child 66234 836898197296
permissions -rw-r--r--
more complete exception handling;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    10
import java.io.{File => JFile}
65188
50cfc6775361 more complete exception handling;
wenzelm
parents: 65069
diff changeset
    11
import java.nio.file.{Paths, FileSystemNotFoundException}
64729
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    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
d83a1eeff9d2 more operations;
wenzelm
parents: 62248
diff changeset
    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
dca0bac351b2 allow single quote within URL;
wenzelm
parents: 56503
diff changeset
    19
  def escape(name: String): String =
dca0bac351b2 allow single quote within URL;
wenzelm
parents: 56503
diff changeset
    20
    (for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString
dca0bac351b2 allow single quote within URL;
wenzelm
parents: 56503
diff changeset
    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
d83a1eeff9d2 more operations;
wenzelm
parents: 62248
diff changeset
    36
d83a1eeff9d2 more operations;
wenzelm
parents: 62248
diff changeset
    37
  /* read */
d83a1eeff9d2 more operations;
wenzelm
parents: 62248
diff changeset
    38
63645
d7e0004d4321 more operations;
wenzelm
parents: 63642
diff changeset
    39
  private def read(url: URL, gzip: Boolean): String =
65069
wenzelm
parents: 64777
diff changeset
    40
    using(url.openStream)(stream =>
wenzelm
parents: 64777
diff changeset
    41
      File.read_stream(if (gzip) new GZIPInputStream(stream) else stream))
63642
d83a1eeff9d2 more operations;
wenzelm
parents: 62248
diff changeset
    42
63645
d7e0004d4321 more operations;
wenzelm
parents: 63642
diff changeset
    43
  def read(url: URL): String = read(url, false)
d7e0004d4321 more operations;
wenzelm
parents: 63642
diff changeset
    44
  def read_gzip(url: URL): String = read(url, true)
d7e0004d4321 more operations;
wenzelm
parents: 63642
diff changeset
    45
d7e0004d4321 more operations;
wenzelm
parents: 63642
diff changeset
    46
  def read(name: String): String = read(Url(name), false)
d7e0004d4321 more operations;
wenzelm
parents: 63642
diff changeset
    47
  def read_gzip(name: String): String = read(Url(name), true)
64729
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    48
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    49
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    50
  /* file URIs */
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    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
dd3797f1e0d6 clarified file URIs;
wenzelm
parents: 64766
diff changeset
    54
dd3797f1e0d6 clarified file URIs;
wenzelm
parents: 64766
diff changeset
    55
  def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
64729
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    56
4eccd9bc5fd9 clarified file URI operations;
wenzelm
parents: 63645
diff changeset
    57
  def is_wellformed_file(uri: String): Boolean =
64775
dd3797f1e0d6 clarified file URIs;
wenzelm
parents: 64766
diff changeset
    58
    try { parse_file(uri); true }
65188
50cfc6775361 more complete exception handling;
wenzelm
parents: 65069
diff changeset
    59
    catch {
50cfc6775361 more complete exception handling;
wenzelm
parents: 65069
diff changeset
    60
      case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException =>
50cfc6775361 more complete exception handling;
wenzelm
parents: 65069
diff changeset
    61
        false
50cfc6775361 more complete exception handling;
wenzelm
parents: 65069
diff changeset
    62
    }
64730
76996d915894 clarified modules;
wenzelm
parents: 64729
diff changeset
    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
}