author | wenzelm |
Fri, 30 Jun 2017 14:01:55 +0200 | |
changeset 66232 | be0ab4b94c62 |
parent 65589 | f70c617e9c26 |
child 66233 | 7188967253e5 |
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, |
14 |
Files, SimpleFileVisitor, FileVisitResult} |
|
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 |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
19 |
|
64002 | 20 |
import org.tukaani.xz.{XZInputStream, XZOutputStream} |
21 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
22 |
import scala.collection.mutable |
60992 | 23 |
import scala.util.matching.Regex |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
24 |
|
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 |
object File |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
27 |
{ |
60992 | 28 |
/* standard path (Cygwin or Posix) */ |
60988 | 29 |
|
30 |
def standard_path(path: Path): String = path.expand.implode |
|
31 |
||
60992 | 32 |
def standard_path(platform_path: String): String = |
33 |
if (Platform.is_windows) { |
|
34 |
val Platform_Root = new Regex("(?i)" + |
|
61291 | 35 |
Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") |
64775 | 36 |
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") |
60992 | 37 |
|
38 |
platform_path.replace('/', '\\') match { |
|
39 |
case Platform_Root(rest) => "/" + rest.replace('\\', '/') |
|
40 |
case Drive(letter, rest) => |
|
41 |
"/cygdrive/" + Word.lowercase(letter) + |
|
42 |
(if (rest == "") "" else "/" + rest.replace('\\', '/')) |
|
43 |
case path => path.replace('\\', '/') |
|
44 |
} |
|
45 |
} |
|
46 |
else platform_path |
|
47 |
||
48 |
def standard_path(file: JFile): String = standard_path(file.getPath) |
|
49 |
||
50 |
def standard_url(name: String): String = |
|
51 |
try { |
|
52 |
val url = new URL(name) |
|
64775 | 53 |
if (url.getProtocol == "file" && Url.is_wellformed_file(name)) |
54 |
standard_path(Url.parse_file(name)) |
|
60992 | 55 |
else name |
56 |
} |
|
57 |
catch { case _: MalformedURLException => standard_path(name) } |
|
58 |
||
59 |
||
60 |
/* platform path (Windows or Posix) */ |
|
61 |
||
62 |
private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") |
|
63 |
private val Named_Root = new Regex("//+([^/]*)(.*)") |
|
64 |
||
65 |
def platform_path(standard_path: String): String = |
|
66 |
if (Platform.is_windows) { |
|
67 |
val result_path = new StringBuilder |
|
68 |
val rest = |
|
69 |
standard_path match { |
|
70 |
case Cygdrive(drive, rest) => |
|
71 |
result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) |
|
72 |
rest |
|
73 |
case Named_Root(root, rest) => |
|
74 |
result_path ++= JFile.separator |
|
75 |
result_path ++= JFile.separator |
|
76 |
result_path ++= root |
|
77 |
rest |
|
78 |
case path if path.startsWith("/") => |
|
61291 | 79 |
result_path ++= Isabelle_System.cygwin_root() |
60992 | 80 |
path |
81 |
case path => path |
|
82 |
} |
|
83 |
for (p <- space_explode('/', rest) if p != "") { |
|
84 |
val len = result_path.length |
|
85 |
if (len > 0 && result_path(len - 1) != JFile.separatorChar) |
|
86 |
result_path += JFile.separatorChar |
|
87 |
result_path ++= p |
|
88 |
} |
|
89 |
result_path.toString |
|
90 |
} |
|
91 |
else standard_path |
|
92 |
||
93 |
def platform_path(path: Path): String = platform_path(standard_path(path)) |
|
60988 | 94 |
def platform_file(path: Path): JFile = new JFile(platform_path(path)) |
95 |
||
60992 | 96 |
|
66232 | 97 |
/* platform files */ |
98 |
||
99 |
def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile |
|
100 |
def canonical(file: JFile): JFile = file.getCanonicalFile |
|
101 |
||
102 |
def path(file: JFile): Path = Path.explode(standard_path(file)) |
|
103 |
def pwd(): Path = path(Path.current.absolute_file) |
|
104 |
||
105 |
||
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
|
106 |
/* bash path */ |
60992 | 107 |
|
64304 | 108 |
def bash_path(path: Path): String = Bash.string(standard_path(path)) |
109 |
def bash_path(file: JFile): String = Bash.string(standard_path(file)) |
|
60988 | 110 |
|
111 |
||
62544 | 112 |
/* directory entries */ |
113 |
||
114 |
def check_dir(path: Path): Path = |
|
115 |
if (path.is_dir) path else error("No such directory: " + path) |
|
116 |
||
117 |
def check_file(path: Path): Path = |
|
118 |
if (path.is_file) path else error("No such file: " + path) |
|
119 |
||
120 |
||
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
121 |
/* directory content */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
122 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
123 |
def read_dir(dir: Path): List[String] = |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
124 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
125 |
if (!dir.is_dir) error("Bad directory: " + dir.toString) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
126 |
val files = dir.file.listFiles |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
127 |
if (files == null) Nil |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
128 |
else files.toList.map(_.getName) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
129 |
} |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
130 |
|
64932 | 131 |
def find_files( |
132 |
start: JFile, |
|
133 |
pred: JFile => Boolean = _ => true, |
|
134 |
include_dirs: Boolean = false): List[JFile] = |
|
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
135 |
{ |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
136 |
val result = new mutable.ListBuffer[JFile] |
64932 | 137 |
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
|
138 |
|
64932 | 139 |
if (start.isFile) check(start) |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
140 |
else if (start.isDirectory) { |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
141 |
Files.walkFileTree(start.toPath, |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
142 |
new SimpleFileVisitor[JPath] { |
64932 | 143 |
override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult = |
144 |
{ |
|
145 |
if (include_dirs) check(path.toFile) |
|
146 |
FileVisitResult.CONTINUE |
|
147 |
} |
|
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
148 |
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
|
149 |
{ |
64932 | 150 |
check(path.toFile) |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
151 |
FileVisitResult.CONTINUE |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
152 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
153 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
154 |
) |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
155 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
156 |
|
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
157 |
result.toList |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
158 |
} |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
159 |
|
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
160 |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
161 |
/* read */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
162 |
|
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
|
163 |
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
|
164 |
def read(path: Path): String = read(path.file) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
165 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
166 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
167 |
def read_stream(reader: BufferedReader): String = |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
168 |
{ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
169 |
val output = new StringBuilder(100) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
170 |
var c = -1 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
171 |
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
|
172 |
reader.close |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
173 |
output.toString |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
174 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
175 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
176 |
def read_stream(stream: InputStream): String = |
64000 | 177 |
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
|
178 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
179 |
def read_gzip(file: JFile): String = |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
180 |
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) |
64000 | 181 |
def read_gzip(path: Path): String = read_gzip(path.file) |
51504 | 182 |
|
64002 | 183 |
def read_xz(file: JFile): String = |
184 |
read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) |
|
64000 | 185 |
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
|
186 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
187 |
|
50845 | 188 |
/* read lines */ |
189 |
||
190 |
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = |
|
191 |
{ |
|
192 |
val result = new mutable.ListBuffer[String] |
|
193 |
var line: String = null |
|
51251
d55cce4d72dd
more permissive File.read_lines, which is relevant for Managed_Process join/kill;
wenzelm
parents:
50845
diff
changeset
|
194 |
while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) { |
50845 | 195 |
progress(line) |
196 |
result += line |
|
197 |
} |
|
198 |
reader.close |
|
199 |
result.toList |
|
200 |
} |
|
201 |
||
202 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
203 |
/* write */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
204 |
|
64002 | 205 |
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
|
206 |
{ |
51504 | 207 |
val stream = make_stream(new FileOutputStream(file)) |
208 |
val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)) |
|
64002 | 209 |
try { writer.append(text) } finally { writer.close } |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
210 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
211 |
|
64003 | 212 |
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
|
213 |
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
|
214 |
|
64002 | 215 |
def write_gzip(file: JFile, text: CharSequence): Unit = |
51504 | 216 |
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) |
48494 | 217 |
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
|
218 |
|
64002 | 219 |
def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit = |
64003 | 220 |
File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) |
221 |
def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options()) |
|
64002 | 222 |
def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit = |
223 |
write_xz(path.file, text, options) |
|
64003 | 224 |
def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options()) |
64000 | 225 |
|
53336 | 226 |
def write_backup(path: Path, text: CharSequence) |
227 |
{ |
|
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
228 |
if (path.is_file) move(path, path.backup) |
62444 | 229 |
write(path, text) |
53336 | 230 |
} |
231 |
||
58610 | 232 |
def write_backup2(path: Path, text: CharSequence) |
233 |
{ |
|
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
234 |
if (path.is_file) move(path, path.backup2) |
62444 | 235 |
write(path, text) |
58610 | 236 |
} |
237 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
238 |
|
62703 | 239 |
/* append */ |
240 |
||
241 |
def append(file: JFile, text: CharSequence): Unit = |
|
242 |
Files.write(file.toPath, UTF8.bytes(text.toString), |
|
243 |
StandardOpenOption.APPEND, StandardOpenOption.CREATE) |
|
244 |
||
245 |
def append(path: Path, text: CharSequence): Unit = append(path.file, text) |
|
246 |
||
247 |
||
64213 | 248 |
/* eq */ |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
249 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
250 |
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
|
251 |
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
|
252 |
catch { case ERROR(_) => false } |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
253 |
|
64213 | 254 |
def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) |
255 |
||
256 |
||
64934 | 257 |
/* eq_content */ |
258 |
||
259 |
def eq_content(file1: JFile, file2: JFile): Boolean = |
|
260 |
if (eq(file1, file2)) true |
|
261 |
else if (file1.length != file2.length) false |
|
262 |
else Bytes.read(file1) == Bytes.read(file2) |
|
263 |
||
264 |
def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) |
|
265 |
||
266 |
||
64213 | 267 |
/* copy */ |
268 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
269 |
def copy(src: JFile, dst: JFile) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
270 |
{ |
61371
17944b500166
clarified, according to Isabelle_System.copy_file in ML;
wenzelm
parents:
61291
diff
changeset
|
271 |
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst |
61373 | 272 |
if (!eq(src, target)) |
273 |
Files.copy(src.toPath, target.toPath, |
|
274 |
StandardCopyOption.COPY_ATTRIBUTES, |
|
275 |
StandardCopyOption.REPLACE_EXISTING) |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
276 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
277 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
278 |
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) |
64213 | 279 |
|
280 |
||
281 |
/* move */ |
|
282 |
||
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
283 |
def move(src: JFile, dst: JFile) |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
284 |
{ |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
285 |
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
|
286 |
if (!eq(src, target)) |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
287 |
Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) |
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
288 |
} |
64213 | 289 |
|
64482
43f6c28ff496
clarified File.move: target directory like File.copy;
wenzelm
parents:
64345
diff
changeset
|
290 |
def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
291 |
} |