6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.io.{File => JFile} |
10 import java.io.{File => JFile} |
|
11 import java.nio.file.Paths |
11 import java.net.{URI, URISyntaxException} |
12 import java.net.{URI, URISyntaxException} |
12 import java.net.{URL, MalformedURLException} |
13 import java.net.{URL, MalformedURLException} |
13 import java.util.zip.GZIPInputStream |
14 import java.util.zip.GZIPInputStream |
14 |
15 |
15 |
16 |
49 def read_gzip(name: String): String = read(Url(name), true) |
50 def read_gzip(name: String): String = read(Url(name), true) |
50 |
51 |
51 |
52 |
52 /* file URIs */ |
53 /* file URIs */ |
53 |
54 |
54 def file(uri: String): JFile = new JFile(new URI(uri)) |
55 def print_file(file: JFile): String = |
|
56 file.toPath.toAbsolutePath.toUri.normalize.toString |
|
57 |
|
58 def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile |
55 |
59 |
56 def is_wellformed_file(uri: String): Boolean = |
60 def is_wellformed_file(uri: String): Boolean = |
57 try { file(uri); true } |
61 try { parse_file(uri); true } |
58 catch { case _: URISyntaxException | _: IllegalArgumentException => false } |
62 catch { case _: URISyntaxException | _: IllegalArgumentException => false } |
59 |
63 |
60 def normalize_file(uri: String): String = |
64 def normalize_file(uri: String): String = |
61 if (is_wellformed_file(uri)) { |
65 if (is_wellformed_file(uri)) print_file(parse_file(uri)) else uri |
62 val uri1 = new URI(uri).normalize.toASCIIString |
|
63 if (uri1.startsWith("file://")) uri1 |
|
64 else { |
|
65 Library.try_unprefix("file:/", uri1) match { |
|
66 case Some(p) => "file:///" + p |
|
67 case None => uri1 |
|
68 } |
|
69 } |
|
70 } |
|
71 else uri |
|
72 |
|
73 def platform_file(path: Path): String = |
|
74 { |
|
75 val path1 = path.expand |
|
76 require(path1.is_absolute) |
|
77 platform_file(File.platform_path(path1)) |
|
78 } |
|
79 |
|
80 def platform_file(name: String): String = |
|
81 if (name.startsWith("file://")) name |
|
82 else { |
|
83 val s = name.replaceAll(" ", "%20") |
|
84 "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s) |
|
85 } |
|
86 } |
66 } |