author | wenzelm |
Mon, 09 Mar 2020 19:35:07 +0100 | |
changeset 71534 | f10bffaa2bae |
parent 71377 | e40f287c25c4 |
child 71601 | 97ccf48c2f0c |
permissions | -rw-r--r-- |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/file.scala |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
3 |
|
64698 | 4 |
File-system operations. |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
6 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
8 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
9 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
10 |
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, |
51504 | 11 |
OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, |
12 |
InputStreamReader, File => JFile, IOException} |
|
62703 | 13 |
import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath, |
69402
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
14 |
Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException} |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
15 |
import java.nio.file.attribute.BasicFileAttributes |
64775 | 16 |
import java.net.{URL, MalformedURLException} |
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
17 |
import java.util.zip.{GZIPInputStream, GZIPOutputStream} |
60992 | 18 |
import java.util.regex.Pattern |
69293
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
19 |
import java.util.EnumSet |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
20 |
|
64002 | 21 |
import org.tukaani.xz.{XZInputStream, XZOutputStream} |
22 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
23 |
import scala.collection.mutable |
60992 | 24 |
import scala.util.matching.Regex |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
25 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
26 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
27 |
object File |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
28 |
{ |
60992 | 29 |
/* standard path (Cygwin or Posix) */ |
60988 | 30 |
|
31 |
def standard_path(path: Path): String = path.expand.implode |
|
32 |
||
60992 | 33 |
def standard_path(platform_path: String): String = |
34 |
if (Platform.is_windows) { |
|
35 |
val Platform_Root = new Regex("(?i)" + |
|
61291 | 36 |
Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") |
64775 | 37 |
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") |
60992 | 38 |
|
39 |
platform_path.replace('/', '\\') match { |
|
40 |
case Platform_Root(rest) => "/" + rest.replace('\\', '/') |
|
41 |
case Drive(letter, rest) => |
|
42 |
"/cygdrive/" + Word.lowercase(letter) + |
|
43 |
(if (rest == "") "" else "/" + rest.replace('\\', '/')) |
|
44 |
case path => path.replace('\\', '/') |
|
45 |
} |
|
46 |
} |
|
47 |
else platform_path |
|
48 |
||
49 |
def standard_path(file: JFile): String = standard_path(file.getPath) |
|
50 |
||
51 |
def standard_url(name: String): String = |
|
52 |
try { |
|
53 |
val url = new URL(name) |
|
64775 | 54 |
if (url.getProtocol == "file" && Url.is_wellformed_file(name)) |
55 |
standard_path(Url.parse_file(name)) |
|
60992 | 56 |
else name |
57 |
} |
|
58 |
catch { case _: MalformedURLException => standard_path(name) } |
|
59 |
||
60 |
||
61 |
/* platform path (Windows or Posix) */ |
|
62 |
||
63 |
private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") |
|
64 |
private val Named_Root = new Regex("//+([^/]*)(.*)") |
|
65 |
||
66 |
def platform_path(standard_path: String): String = |
|
67 |
if (Platform.is_windows) { |
|
68 |
val result_path = new StringBuilder |
|
69 |
val rest = |
|
70 |
standard_path match { |
|
71 |
case Cygdrive(drive, rest) => |
|
72 |
result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) |
|
73 |
rest |
|
74 |
case Named_Root(root, rest) => |
|
75 |
result_path ++= JFile.separator |
|
76 |
result_path ++= JFile.separator |
|
77 |
result_path ++= root |
|
78 |
rest |
|
79 |
case path if path.startsWith("/") => |
|
61291 | 80 |
result_path ++= Isabelle_System.cygwin_root() |
60992 | 81 |
path |
82 |
case path => path |
|
83 |
} |
|
84 |
for (p <- space_explode('/', rest) if p != "") { |
|
85 |
val len = result_path.length |
|
86 |
if (len > 0 && result_path(len - 1) != JFile.separatorChar) |
|
87 |
result_path += JFile.separatorChar |
|
88 |
result_path ++= p |
|
89 |
} |
|
90 |
result_path.toString |
|
91 |
} |
|
92 |
else standard_path |
|
93 |
||
94 |
def platform_path(path: Path): String = platform_path(standard_path(path)) |
|
60988 | 95 |
def platform_file(path: Path): JFile = new JFile(platform_path(path)) |
96 |
||
60992 | 97 |
|
66232 | 98 |
/* platform files */ |
99 |
||
100 |
def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile |
|
66233 | 101 |
def absolute_name(file: JFile): String = absolute(file).getPath |
102 |
||
66232 | 103 |
def canonical(file: JFile): JFile = file.getCanonicalFile |
66233 | 104 |
def canonical_name(file: JFile): String = canonical(file).getPath |
66232 | 105 |
|
106 |
def path(file: JFile): Path = Path.explode(standard_path(file)) |
|
107 |
def pwd(): Path = path(Path.current.absolute_file) |
|
108 |
||
109 |
||
66693 | 110 |
/* relative paths */ |
111 |
||
112 |
def relative_path(base: Path, other: Path): Option[Path] = |
|
113 |
{ |
|
114 |
val base_path = base.file.toPath |
|
115 |
val other_path = other.file.toPath |
|
116 |
if (other_path.startsWith(base_path)) |
|
117 |
Some(path(base_path.relativize(other_path).toFile)) |
|
118 |
else None |
|
119 |
} |
|
120 |
||
121 |
||
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
122 |
/* bash path */ |
60992 | 123 |
|
64304 | 124 |
def bash_path(path: Path): String = Bash.string(standard_path(path)) |
125 |
def bash_path(file: JFile): String = Bash.string(standard_path(file)) |
|
60988 | 126 |
|
127 |
||
62544 | 128 |
/* directory entries */ |
129 |
||
130 |
def check_dir(path: Path): Path = |
|
131 |
if (path.is_dir) path else error("No such directory: " + path) |
|
132 |
||
133 |
def check_file(path: Path): Path = |
|
134 |
if (path.is_file) path else error("No such file: " + path) |
|
135 |
||
136 |
||
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
137 |
/* directory content */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
138 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
139 |
def read_dir(dir: Path): List[String] = |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
140 |
{ |
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69299
diff
changeset
|
141 |
if (!dir.is_dir) error("No such directory: " + dir.toString) |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
142 |
val files = dir.file.listFiles |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
143 |
if (files == null) Nil |
69427
ff2f39a221d4
clarified operations: uniform sorting of results;
wenzelm
parents:
69405
diff
changeset
|
144 |
else files.toList.map(_.getName).sorted |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
145 |
} |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
146 |
|
64932 | 147 |
def find_files( |
148 |
start: JFile, |
|
149 |
pred: JFile => Boolean = _ => true, |
|
69293
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
150 |
include_dirs: Boolean = false, |
69299
2fd070377c99
clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
wenzelm
parents:
69293
diff
changeset
|
151 |
follow_links: Boolean = false): List[JFile] = |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
152 |
{ |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
153 |
val result = new mutable.ListBuffer[JFile] |
64932 | 154 |
def check(file: JFile) { if (pred(file)) result += file } |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
155 |
|
64932 | 156 |
if (start.isFile) check(start) |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
157 |
else if (start.isDirectory) { |
69293
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
158 |
val options = |
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
159 |
if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) |
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
160 |
else EnumSet.noneOf(classOf[FileVisitOption]) |
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
161 |
Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
162 |
new SimpleFileVisitor[JPath] { |
64932 | 163 |
override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult = |
164 |
{ |
|
165 |
if (include_dirs) check(path.toFile) |
|
166 |
FileVisitResult.CONTINUE |
|
167 |
} |
|
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
168 |
override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult = |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
169 |
{ |
69301 | 170 |
val file = path.toFile |
171 |
if (include_dirs || !file.isDirectory) check(file) |
|
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
172 |
FileVisitResult.CONTINUE |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
173 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
174 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
175 |
) |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
176 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
177 |
|
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
178 |
result.toList |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
179 |
} |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
180 |
|
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
181 |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
182 |
/* read */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
183 |
|
65589
f70c617e9c26
more robust treatment of non-UTF8 text files (cf. 3ed43cfc8b14), notably old log files in ISO-8859-15;
wenzelm
parents:
64934
diff
changeset
|
184 |
def read(file: JFile): String = Bytes.read(file).text |
48913
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
185 |
def read(path: Path): String = read(path.file) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
186 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
187 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
188 |
def read_stream(reader: BufferedReader): String = |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
189 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
190 |
val output = new StringBuilder(100) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
191 |
var c = -1 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
192 |
while ({ c = reader.read; c != -1 }) output += c.toChar |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
193 |
reader.close |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
194 |
output.toString |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
195 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
196 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
197 |
def read_stream(stream: InputStream): String = |
64000 | 198 |
read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) |
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
199 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
200 |
def read_gzip(file: JFile): String = |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
201 |
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) |
64000 | 202 |
def read_gzip(path: Path): String = read_gzip(path.file) |
51504 | 203 |
|
64002 | 204 |
def read_xz(file: JFile): String = |
205 |
read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) |
|
64000 | 206 |
def read_xz(path: Path): String = read_xz(path.file) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
207 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
208 |
|
50845 | 209 |
/* read lines */ |
210 |
||
69487 | 211 |
def read_line(reader: BufferedReader): Option[String] = |
212 |
{ |
|
213 |
val line = |
|
214 |
try { reader.readLine} |
|
215 |
catch { case _: IOException => null } |
|
216 |
if (line == null) None else Some(line) |
|
217 |
} |
|
218 |
||
50845 | 219 |
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = |
220 |
{ |
|
221 |
val result = new mutable.ListBuffer[String] |
|
69487 | 222 |
var line: Option[String] = None |
223 |
while ({ line = read_line(reader); line.isDefined }) { |
|
224 |
progress(line.get) |
|
225 |
result += line.get |
|
50845 | 226 |
} |
227 |
reader.close |
|
228 |
result.toList |
|
229 |
} |
|
230 |
||
231 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
232 |
/* write */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
233 |
|
71534 | 234 |
def writer(file: JFile): BufferedWriter = |
235 |
new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset)) |
|
236 |
||
64002 | 237 |
def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
238 |
{ |
51504 | 239 |
val stream = make_stream(new FileOutputStream(file)) |
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69301
diff
changeset
|
240 |
using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
241 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
242 |
|
64003 | 243 |
def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
244 |
def write(path: Path, text: CharSequence): Unit = write(path.file, text) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
245 |
|
64002 | 246 |
def write_gzip(file: JFile, text: CharSequence): Unit = |
51504 | 247 |
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) |
48494 | 248 |
def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
249 |
|
64002 | 250 |
def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit = |
64003 | 251 |
File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) |
252 |
def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options()) |
|
64002 | 253 |
def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit = |
254 |
write_xz(path.file, text, options) |
|
64003 | 255 |
def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options()) |
64000 | 256 |
|
53336 | 257 |
def write_backup(path: Path, text: CharSequence) |
258 |
{ |
|
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
259 |
if (path.is_file) move(path, path.backup) |
62444 | 260 |
write(path, text) |
53336 | 261 |
} |
262 |
||
58610 | 263 |
def write_backup2(path: Path, text: CharSequence) |
264 |
{ |
|
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
265 |
if (path.is_file) move(path, path.backup2) |
62444 | 266 |
write(path, text) |
58610 | 267 |
} |
268 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
269 |
|
62703 | 270 |
/* append */ |
271 |
||
272 |
def append(file: JFile, text: CharSequence): Unit = |
|
273 |
Files.write(file.toPath, UTF8.bytes(text.toString), |
|
274 |
StandardOpenOption.APPEND, StandardOpenOption.CREATE) |
|
275 |
||
276 |
def append(path: Path, text: CharSequence): Unit = append(path.file, text) |
|
277 |
||
278 |
||
64213 | 279 |
/* eq */ |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
280 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
281 |
def eq(file1: JFile, file2: JFile): Boolean = |
49673
2a088cff1e7b
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents:
49610
diff
changeset
|
282 |
try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } |
2a088cff1e7b
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents:
49610
diff
changeset
|
283 |
catch { case ERROR(_) => false } |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
284 |
|
64213 | 285 |
def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) |
286 |
||
287 |
||
64934 | 288 |
/* eq_content */ |
289 |
||
290 |
def eq_content(file1: JFile, file2: JFile): Boolean = |
|
291 |
if (eq(file1, file2)) true |
|
292 |
else if (file1.length != file2.length) false |
|
293 |
else Bytes.read(file1) == Bytes.read(file2) |
|
294 |
||
295 |
def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) |
|
296 |
||
297 |
||
64213 | 298 |
/* copy */ |
299 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
300 |
def copy(src: JFile, dst: JFile) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
301 |
{ |
61371
17944b500166
clarified, according to Isabelle_System.copy_file in ML;
wenzelm
parents:
61291
diff
changeset
|
302 |
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst |
61373 | 303 |
if (!eq(src, target)) |
304 |
Files.copy(src.toPath, target.toPath, |
|
305 |
StandardCopyOption.COPY_ATTRIBUTES, |
|
306 |
StandardCopyOption.REPLACE_EXISTING) |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
307 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
308 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
309 |
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) |
64213 | 310 |
|
311 |
||
312 |
/* move */ |
|
313 |
||
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
314 |
def move(src: JFile, dst: JFile) |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
315 |
{ |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
316 |
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
317 |
if (!eq(src, target)) |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
318 |
Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
319 |
} |
64213 | 320 |
|
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
321 |
def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file) |
69402
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
322 |
|
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
323 |
|
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
324 |
/* symbolic link */ |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
325 |
|
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
326 |
def link(src: Path, dst: Path, force: Boolean = false) |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
327 |
{ |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
328 |
val src_file = src.file |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
329 |
val dst_file = dst.file |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
330 |
val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
331 |
|
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
332 |
if (force) target.delete |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
333 |
|
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
334 |
try { Files.createSymbolicLink(target.toPath, src_file.toPath) } |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
335 |
catch { |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
336 |
case _: UnsupportedOperationException if Platform.is_windows => |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
337 |
Cygwin.link(standard_path(src), target) |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
338 |
case _: FileSystemException if Platform.is_windows => |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
339 |
Cygwin.link(standard_path(src), target) |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
340 |
} |
61f4c406d727
more direct File.link operation: avoid external process;
wenzelm
parents:
69393
diff
changeset
|
341 |
} |
69405
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
342 |
|
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
343 |
|
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
344 |
/* permissions */ |
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
345 |
|
69788 | 346 |
def is_executable(path: Path): Boolean = |
347 |
{ |
|
348 |
if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok |
|
349 |
else path.file.canExecute |
|
350 |
} |
|
351 |
||
69789
2c3e5e58d93f
more thorough File.set_executable, notably for Windows;
wenzelm
parents:
69788
diff
changeset
|
352 |
def set_executable(path: Path, flag: Boolean) |
69405
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
353 |
{ |
71114 | 354 |
if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) |
355 |
else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) |
|
69789
2c3e5e58d93f
more thorough File.set_executable, notably for Windows;
wenzelm
parents:
69788
diff
changeset
|
356 |
else path.file.setExecutable(flag, false) |
69405
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
357 |
} |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
358 |
} |