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