author | wenzelm |
Mon, 07 Mar 2016 20:44:47 +0100 | |
changeset 62548 | f8ebb715e06d |
parent 62545 | 8ebffdaf2ce2 |
child 62636 | e676ae9f1bf6 |
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 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
4 |
File system operations. |
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} |
|
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
13 |
import java.nio.file.{StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitResult} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
14 |
import java.nio.file.attribute.BasicFileAttributes |
60992 | 15 |
import java.net.{URL, URLDecoder, MalformedURLException} |
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
16 |
import java.util.zip.{GZIPInputStream, GZIPOutputStream} |
60992 | 17 |
import java.util.regex.Pattern |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
18 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
19 |
import scala.collection.mutable |
60992 | 20 |
import scala.util.matching.Regex |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
21 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
22 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
23 |
object File |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
24 |
{ |
60992 | 25 |
/* standard path (Cygwin or Posix) */ |
60988 | 26 |
|
27 |
def standard_path(path: Path): String = path.expand.implode |
|
28 |
||
60992 | 29 |
def standard_path(platform_path: String): String = |
30 |
if (Platform.is_windows) { |
|
31 |
val Platform_Root = new Regex("(?i)" + |
|
61291 | 32 |
Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") |
60992 | 33 |
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") |
34 |
||
35 |
platform_path.replace('/', '\\') match { |
|
36 |
case Platform_Root(rest) => "/" + rest.replace('\\', '/') |
|
37 |
case Drive(letter, rest) => |
|
38 |
"/cygdrive/" + Word.lowercase(letter) + |
|
39 |
(if (rest == "") "" else "/" + rest.replace('\\', '/')) |
|
40 |
case path => path.replace('\\', '/') |
|
41 |
} |
|
42 |
} |
|
43 |
else platform_path |
|
44 |
||
45 |
def standard_path(file: JFile): String = standard_path(file.getPath) |
|
46 |
||
47 |
def standard_url(name: String): String = |
|
48 |
try { |
|
49 |
val url = new URL(name) |
|
50 |
if (url.getProtocol == "file") |
|
51 |
standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name)) |
|
52 |
else name |
|
53 |
} |
|
54 |
catch { case _: MalformedURLException => standard_path(name) } |
|
55 |
||
56 |
||
57 |
/* platform path (Windows or Posix) */ |
|
58 |
||
59 |
private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") |
|
60 |
private val Named_Root = new Regex("//+([^/]*)(.*)") |
|
61 |
||
62 |
def platform_path(standard_path: String): String = |
|
63 |
if (Platform.is_windows) { |
|
64 |
val result_path = new StringBuilder |
|
65 |
val rest = |
|
66 |
standard_path match { |
|
67 |
case Cygdrive(drive, rest) => |
|
68 |
result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) |
|
69 |
rest |
|
70 |
case Named_Root(root, rest) => |
|
71 |
result_path ++= JFile.separator |
|
72 |
result_path ++= JFile.separator |
|
73 |
result_path ++= root |
|
74 |
rest |
|
75 |
case path if path.startsWith("/") => |
|
61291 | 76 |
result_path ++= Isabelle_System.cygwin_root() |
60992 | 77 |
path |
78 |
case path => path |
|
79 |
} |
|
80 |
for (p <- space_explode('/', rest) if p != "") { |
|
81 |
val len = result_path.length |
|
82 |
if (len > 0 && result_path(len - 1) != JFile.separatorChar) |
|
83 |
result_path += JFile.separatorChar |
|
84 |
result_path ++= p |
|
85 |
} |
|
86 |
result_path.toString |
|
87 |
} |
|
88 |
else standard_path |
|
89 |
||
90 |
def platform_path(path: Path): String = platform_path(standard_path(path)) |
|
60988 | 91 |
def platform_file(path: Path): JFile = new JFile(platform_path(path)) |
92 |
||
60992 | 93 |
def platform_url(raw_path: Path): String = |
60988 | 94 |
{ |
95 |
val path = raw_path.expand |
|
96 |
require(path.is_absolute) |
|
97 |
val s = platform_path(path).replaceAll(" ", "%20") |
|
98 |
if (!Platform.is_windows) "file://" + s |
|
99 |
else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/') |
|
100 |
else "file:///" + s.replace('\\', '/') |
|
101 |
} |
|
102 |
||
60992 | 103 |
|
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
|
104 |
/* bash path */ |
60992 | 105 |
|
62548 | 106 |
private def bash_chr(c: Byte): String = |
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
|
107 |
{ |
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
|
108 |
val ch = c.toChar |
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
|
109 |
ch match { |
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
|
110 |
case '\t' => "$'\\t'" |
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
|
111 |
case '\n' => "$'\\n'" |
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
|
112 |
case '\f' => "$'\\f'" |
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
|
113 |
case '\r' => "$'\\r'" |
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
|
114 |
case _ => |
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
|
115 |
if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch)) |
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
|
116 |
Symbol.ascii(ch) |
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
|
117 |
else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" |
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
|
118 |
else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" |
62548 | 119 |
else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" |
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
|
120 |
else "\\" + ch |
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
|
121 |
} |
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 |
} |
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
|
123 |
|
62548 | 124 |
def bash_string(s: String): String = |
125 |
UTF8.bytes(s).iterator.map(bash_chr(_)).mkString |
|
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
|
126 |
|
62548 | 127 |
def bash_args(args: List[String]): String = |
128 |
args.iterator.map(bash_string(_)).mkString(" ") |
|
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
|
129 |
|
62548 | 130 |
def bash_path(path: Path): String = bash_string(standard_path(path)) |
131 |
def bash_path(file: JFile): String = bash_string(standard_path(file)) |
|
60988 | 132 |
|
133 |
||
62544 | 134 |
/* directory entries */ |
135 |
||
136 |
def check_dir(path: Path): Path = |
|
137 |
if (path.is_dir) path else error("No such directory: " + path) |
|
138 |
||
139 |
def check_file(path: Path): Path = |
|
140 |
if (path.is_file) path else error("No such file: " + path) |
|
141 |
||
142 |
||
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
143 |
/* find files */ |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
144 |
|
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
145 |
def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] = |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
146 |
{ |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
147 |
val result = new mutable.ListBuffer[JFile] |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
148 |
|
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
149 |
if (start.isFile && pred(start)) result += start |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
150 |
else if (start.isDirectory) { |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
151 |
Files.walkFileTree(start.toPath, |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
152 |
new SimpleFileVisitor[JPath] { |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
153 |
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
|
154 |
{ |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
155 |
val file = path.toFile |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
156 |
if (pred(file)) result += file |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
157 |
FileVisitResult.CONTINUE |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
158 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
159 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
160 |
) |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
161 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
162 |
|
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
163 |
result.toList |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
164 |
} |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
165 |
|
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
166 |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
167 |
/* read */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
168 |
|
54440 | 169 |
def read(file: JFile): String = Bytes.read(file).toString |
48913
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
170 |
def read(path: Path): String = read(path.file) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
171 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
172 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
173 |
def read_stream(reader: BufferedReader): String = |
48411
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 |
val output = new StringBuilder(100) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
176 |
var c = -1 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
177 |
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
|
178 |
reader.close |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
179 |
output.toString |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
180 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
181 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
182 |
def read_stream(stream: InputStream): String = |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
183 |
read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
184 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
185 |
def read_gzip(file: JFile): String = |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
186 |
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) |
51504 | 187 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
188 |
def read_gzip(path: Path): String = read_gzip(path.file) |
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 |
|
50845 | 191 |
/* read lines */ |
192 |
||
193 |
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = |
|
194 |
{ |
|
195 |
val result = new mutable.ListBuffer[String] |
|
196 |
var line: String = null |
|
51251
d55cce4d72dd
more permissive File.read_lines, which is relevant for Managed_Process join/kill;
wenzelm
parents:
50845
diff
changeset
|
197 |
while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) { |
50845 | 198 |
progress(line) |
199 |
result += line |
|
200 |
} |
|
201 |
reader.close |
|
202 |
result.toList |
|
203 |
} |
|
204 |
||
205 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
206 |
/* write */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
207 |
|
52671
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
51982
diff
changeset
|
208 |
def write_file(file: JFile, text: Iterable[CharSequence], |
51982 | 209 |
make_stream: OutputStream => OutputStream) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
210 |
{ |
51504 | 211 |
val stream = make_stream(new FileOutputStream(file)) |
212 |
val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)) |
|
51982 | 213 |
try { text.iterator.foreach(writer.append(_)) } |
214 |
finally { writer.close } |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
215 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
216 |
|
51982 | 217 |
def write(file: JFile, text: Iterable[CharSequence]): Unit = write_file(file, text, (s) => s) |
218 |
def write(file: JFile, text: CharSequence): Unit = write(file, List(text)) |
|
219 |
def write(path: Path, text: Iterable[CharSequence]): Unit = write(path.file, text) |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
220 |
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
|
221 |
|
51982 | 222 |
def write_gzip(file: JFile, text: Iterable[CharSequence]): Unit = |
51504 | 223 |
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) |
51982 | 224 |
def write_gzip(file: JFile, text: CharSequence): Unit = write_gzip(file, List(text)) |
225 |
def write_gzip(path: Path, text: Iterable[CharSequence]): Unit = write_gzip(path.file, text) |
|
48494 | 226 |
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
|
227 |
|
53336 | 228 |
def write_backup(path: Path, text: CharSequence) |
229 |
{ |
|
230 |
path.file renameTo path.backup.file |
|
62444 | 231 |
write(path, text) |
53336 | 232 |
} |
233 |
||
58610 | 234 |
def write_backup2(path: Path, text: CharSequence) |
235 |
{ |
|
236 |
path.file renameTo path.backup2.file |
|
62444 | 237 |
write(path, text) |
58610 | 238 |
} |
239 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
240 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
241 |
/* copy */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
242 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
243 |
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
|
244 |
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
|
245 |
catch { case ERROR(_) => false } |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
246 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
247 |
def copy(src: JFile, dst: JFile) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
248 |
{ |
61371
17944b500166
clarified, according to Isabelle_System.copy_file in ML;
wenzelm
parents:
61291
diff
changeset
|
249 |
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst |
61373 | 250 |
if (!eq(src, target)) |
251 |
Files.copy(src.toPath, target.toPath, |
|
252 |
StandardCopyOption.COPY_ATTRIBUTES, |
|
253 |
StandardCopyOption.REPLACE_EXISTING) |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
254 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
255 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
256 |
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
257 |
} |