equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
|
10 import java.io.{File => JFile} |
|
11 import java.net.{URI, URISyntaxException} |
10 import java.net.{URL, MalformedURLException} |
12 import java.net.{URL, MalformedURLException} |
11 import java.util.zip.GZIPInputStream |
13 import java.util.zip.GZIPInputStream |
12 |
14 |
13 |
15 |
14 object Url |
16 object Url |
43 def read(url: URL): String = read(url, false) |
45 def read(url: URL): String = read(url, false) |
44 def read_gzip(url: URL): String = read(url, true) |
46 def read_gzip(url: URL): String = read(url, true) |
45 |
47 |
46 def read(name: String): String = read(Url(name), false) |
48 def read(name: String): String = read(Url(name), false) |
47 def read_gzip(name: String): String = read(Url(name), true) |
49 def read_gzip(name: String): String = read(Url(name), true) |
|
50 |
|
51 |
|
52 /* file URIs */ |
|
53 |
|
54 def file(uri: String): JFile = new JFile(new URI(uri)) |
|
55 |
|
56 def is_wellformed_file(uri: String): Boolean = |
|
57 try { file(uri); true } |
|
58 catch { case _: URISyntaxException | _: IllegalArgumentException => false } |
48 } |
59 } |