| author | wenzelm | 
| Fri, 09 Oct 2015 16:29:18 +0200 | |
| changeset 61373 | 16ed9b97c72d | 
| parent 61371 | 17944b500166 | 
| child 61959 | 364007370bb7 | 
| 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}  | 
|
| 61373 | 13  | 
import java.nio.file.{StandardCopyOption, Files}
 | 
| 60992 | 14  | 
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
 | 
15  | 
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 | 
| 60992 | 16  | 
import java.util.regex.Pattern  | 
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
|
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
import scala.collection.mutable  | 
| 60992 | 19  | 
import scala.util.matching.Regex  | 
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
20  | 
|
| 
 
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  | 
object File  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
{
 | 
| 60992 | 24  | 
/* standard path (Cygwin or Posix) */  | 
| 60988 | 25  | 
|
26  | 
def standard_path(path: Path): String = path.expand.implode  | 
|
27  | 
||
| 60992 | 28  | 
def standard_path(platform_path: String): String =  | 
29  | 
    if (Platform.is_windows) {
 | 
|
30  | 
      val Platform_Root = new Regex("(?i)" +
 | 
|
| 61291 | 31  | 
Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")  | 
| 60992 | 32  | 
      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
 | 
33  | 
||
34  | 
      platform_path.replace('/', '\\') match {
 | 
|
35  | 
        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
 | 
|
36  | 
case Drive(letter, rest) =>  | 
|
37  | 
"/cygdrive/" + Word.lowercase(letter) +  | 
|
38  | 
            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
 | 
|
39  | 
        case path => path.replace('\\', '/')
 | 
|
40  | 
}  | 
|
41  | 
}  | 
|
42  | 
else platform_path  | 
|
43  | 
||
44  | 
def standard_path(file: JFile): String = standard_path(file.getPath)  | 
|
45  | 
||
46  | 
def standard_url(name: String): String =  | 
|
47  | 
    try {
 | 
|
48  | 
val url = new URL(name)  | 
|
49  | 
if (url.getProtocol == "file")  | 
|
50  | 
standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name))  | 
|
51  | 
else name  | 
|
52  | 
}  | 
|
53  | 
    catch { case _: MalformedURLException => standard_path(name) }
 | 
|
54  | 
||
55  | 
||
56  | 
/* platform path (Windows or Posix) */  | 
|
57  | 
||
58  | 
  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
 | 
|
59  | 
  private val Named_Root = new Regex("//+([^/]*)(.*)")
 | 
|
60  | 
||
61  | 
def platform_path(standard_path: String): String =  | 
|
62  | 
    if (Platform.is_windows) {
 | 
|
63  | 
val result_path = new StringBuilder  | 
|
64  | 
val rest =  | 
|
65  | 
        standard_path match {
 | 
|
66  | 
case Cygdrive(drive, rest) =>  | 
|
67  | 
result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)  | 
|
68  | 
rest  | 
|
69  | 
case Named_Root(root, rest) =>  | 
|
70  | 
result_path ++= JFile.separator  | 
|
71  | 
result_path ++= JFile.separator  | 
|
72  | 
result_path ++= root  | 
|
73  | 
rest  | 
|
74  | 
          case path if path.startsWith("/") =>
 | 
|
| 61291 | 75  | 
result_path ++= Isabelle_System.cygwin_root()  | 
| 60992 | 76  | 
path  | 
77  | 
case path => path  | 
|
78  | 
}  | 
|
79  | 
      for (p <- space_explode('/', rest) if p != "") {
 | 
|
80  | 
val len = result_path.length  | 
|
81  | 
if (len > 0 && result_path(len - 1) != JFile.separatorChar)  | 
|
82  | 
result_path += JFile.separatorChar  | 
|
83  | 
result_path ++= p  | 
|
84  | 
}  | 
|
85  | 
result_path.toString  | 
|
86  | 
}  | 
|
87  | 
else standard_path  | 
|
88  | 
||
89  | 
def platform_path(path: Path): String = platform_path(standard_path(path))  | 
|
| 60988 | 90  | 
def platform_file(path: Path): JFile = new JFile(platform_path(path))  | 
91  | 
||
| 60992 | 92  | 
def platform_url(raw_path: Path): String =  | 
| 60988 | 93  | 
  {
 | 
94  | 
val path = raw_path.expand  | 
|
95  | 
require(path.is_absolute)  | 
|
96  | 
    val s = platform_path(path).replaceAll(" ", "%20")
 | 
|
97  | 
if (!Platform.is_windows) "file://" + s  | 
|
98  | 
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
 | 
|
99  | 
    else "file:///" + s.replace('\\', '/')
 | 
|
100  | 
}  | 
|
101  | 
||
| 60992 | 102  | 
|
103  | 
/* shell path (bash) */  | 
|
104  | 
||
| 60988 | 105  | 
def shell_path(path: Path): String = "'" + standard_path(path) + "'"  | 
| 60992 | 106  | 
def shell_path(file: JFile): String = "'" + standard_path(file) + "'"  | 
| 60988 | 107  | 
|
108  | 
||
| 
48613
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
109  | 
/* directory content */  | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
110  | 
|
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
111  | 
def read_dir(dir: Path): List[String] =  | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
112  | 
  {
 | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
113  | 
    if (!dir.is_dir) error("Bad directory: " + dir.toString)
 | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
114  | 
val files = dir.file.listFiles  | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
115  | 
if (files == null) Nil  | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
116  | 
else files.toList.map(_.getName)  | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
117  | 
}  | 
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
118  | 
|
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
119  | 
def find_files(dir: Path): Stream[Path] =  | 
| 
56783
 
afaec818fcfd
ignore malformed file names outright, e.g. .class files with dollar;
 
wenzelm 
parents: 
56428 
diff
changeset
 | 
120  | 
read_dir(dir).toStream.map(name =>  | 
| 
 
afaec818fcfd
ignore malformed file names outright, e.g. .class files with dollar;
 
wenzelm 
parents: 
56428 
diff
changeset
 | 
121  | 
      if (Path.is_wellformed(name)) {
 | 
| 
 
afaec818fcfd
ignore malformed file names outright, e.g. .class files with dollar;
 
wenzelm 
parents: 
56428 
diff
changeset
 | 
122  | 
val path = dir + Path.basic(name)  | 
| 
 
afaec818fcfd
ignore malformed file names outright, e.g. .class files with dollar;
 
wenzelm 
parents: 
56428 
diff
changeset
 | 
123  | 
path #:: (if (path.is_dir) find_files(path) else Stream.empty)  | 
| 
 
afaec818fcfd
ignore malformed file names outright, e.g. .class files with dollar;
 
wenzelm 
parents: 
56428 
diff
changeset
 | 
124  | 
}  | 
| 
 
afaec818fcfd
ignore malformed file names outright, e.g. .class files with dollar;
 
wenzelm 
parents: 
56428 
diff
changeset
 | 
125  | 
else Stream.empty).flatten  | 
| 
48613
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
126  | 
|
| 
 
232652ac346e
clarified directory content operations (similar to ML version);
 
wenzelm 
parents: 
48550 
diff
changeset
 | 
127  | 
|
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
128  | 
/* read */  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
129  | 
|
| 54440 | 130  | 
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
 | 
131  | 
def read(path: Path): String = read(path.file)  | 
| 
 
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
 
wenzelm 
parents: 
48613 
diff
changeset
 | 
132  | 
|
| 
50684
 
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
 
wenzelm 
parents: 
50203 
diff
changeset
 | 
133  | 
|
| 
 
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
 
wenzelm 
parents: 
50203 
diff
changeset
 | 
134  | 
def read_stream(reader: BufferedReader): String =  | 
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
135  | 
  {
 | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
136  | 
val output = new StringBuilder(100)  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
137  | 
var c = -1  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
138  | 
    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
 | 
139  | 
reader.close  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
140  | 
output.toString  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
141  | 
}  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
142  | 
|
| 
50684
 
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
 
wenzelm 
parents: 
50203 
diff
changeset
 | 
143  | 
def read_stream(stream: InputStream): String =  | 
| 
 
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
 
wenzelm 
parents: 
50203 
diff
changeset
 | 
144  | 
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
 | 
145  | 
|
| 
 
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
 
wenzelm 
parents: 
50203 
diff
changeset
 | 
146  | 
def read_gzip(file: JFile): String =  | 
| 
 
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
 
wenzelm 
parents: 
50203 
diff
changeset
 | 
147  | 
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))  | 
| 51504 | 148  | 
|
| 
50684
 
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
 
wenzelm 
parents: 
50203 
diff
changeset
 | 
149  | 
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
 | 
150  | 
|
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
151  | 
|
| 50845 | 152  | 
/* read lines */  | 
153  | 
||
154  | 
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =  | 
|
155  | 
  {
 | 
|
156  | 
val result = new mutable.ListBuffer[String]  | 
|
157  | 
var line: String = null  | 
|
| 
51251
 
d55cce4d72dd
more permissive File.read_lines, which is relevant for Managed_Process join/kill;
 
wenzelm 
parents: 
50845 
diff
changeset
 | 
158  | 
    while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) {
 | 
| 50845 | 159  | 
progress(line)  | 
160  | 
result += line  | 
|
161  | 
}  | 
|
162  | 
reader.close  | 
|
163  | 
result.toList  | 
|
164  | 
}  | 
|
165  | 
||
166  | 
||
| 48550 | 167  | 
/* try_read */  | 
168  | 
||
169  | 
def try_read(paths: Seq[Path]): String =  | 
|
170  | 
  {
 | 
|
171  | 
val buf = new StringBuilder  | 
|
172  | 
    for (path <- paths if path.is_file) {
 | 
|
173  | 
buf.append(read(path))  | 
|
174  | 
      buf.append('\n')
 | 
|
175  | 
}  | 
|
176  | 
buf.toString  | 
|
177  | 
}  | 
|
178  | 
||
179  | 
||
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
180  | 
/* write */  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
181  | 
|
| 
52671
 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 
wenzelm 
parents: 
51982 
diff
changeset
 | 
182  | 
def write_file(file: JFile, text: Iterable[CharSequence],  | 
| 51982 | 183  | 
make_stream: OutputStream => OutputStream)  | 
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
184  | 
  {
 | 
| 51504 | 185  | 
val stream = make_stream(new FileOutputStream(file))  | 
186  | 
val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset))  | 
|
| 51982 | 187  | 
    try { text.iterator.foreach(writer.append(_)) }
 | 
188  | 
    finally { writer.close }
 | 
|
| 
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  | 
|
| 51982 | 191  | 
def write(file: JFile, text: Iterable[CharSequence]): Unit = write_file(file, text, (s) => s)  | 
192  | 
def write(file: JFile, text: CharSequence): Unit = write(file, List(text))  | 
|
193  | 
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
 | 
194  | 
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
 | 
195  | 
|
| 51982 | 196  | 
def write_gzip(file: JFile, text: Iterable[CharSequence]): Unit =  | 
| 51504 | 197  | 
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))  | 
| 51982 | 198  | 
def write_gzip(file: JFile, text: CharSequence): Unit = write_gzip(file, List(text))  | 
199  | 
def write_gzip(path: Path, text: Iterable[CharSequence]): Unit = write_gzip(path.file, text)  | 
|
| 48494 | 200  | 
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
 | 
201  | 
|
| 53336 | 202  | 
def write_backup(path: Path, text: CharSequence)  | 
203  | 
  {
 | 
|
204  | 
path.file renameTo path.backup.file  | 
|
205  | 
File.write(path, text)  | 
|
206  | 
}  | 
|
207  | 
||
| 58610 | 208  | 
def write_backup2(path: Path, text: CharSequence)  | 
209  | 
  {
 | 
|
210  | 
path.file renameTo path.backup2.file  | 
|
211  | 
File.write(path, text)  | 
|
212  | 
}  | 
|
213  | 
||
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
214  | 
|
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
215  | 
/* copy */  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
216  | 
|
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
217  | 
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
 | 
218  | 
    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
 | 
219  | 
    catch { case ERROR(_) => false }
 | 
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
220  | 
|
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
221  | 
def copy(src: JFile, dst: JFile)  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
222  | 
  {
 | 
| 
61371
 
17944b500166
clarified, according to Isabelle_System.copy_file in ML;
 
wenzelm 
parents: 
61291 
diff
changeset
 | 
223  | 
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst  | 
| 61373 | 224  | 
if (!eq(src, target))  | 
225  | 
Files.copy(src.toPath, target.toPath,  | 
|
226  | 
StandardCopyOption.COPY_ATTRIBUTES,  | 
|
227  | 
StandardCopyOption.REPLACE_EXISTING)  | 
|
| 
48411
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
228  | 
}  | 
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
229  | 
|
| 
 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 
wenzelm 
parents:  
diff
changeset
 | 
230  | 
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
 | 
231  | 
}  |