author | wenzelm |
Fri, 16 Jun 2023 14:01:30 +0200 | |
changeset 78169 | 5ad1ae8626de |
parent 78161 | 4b1b7cbb3e9a |
child 78243 | 0e221a8128e4 |
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} |
|
73317 | 13 |
import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor, |
14 |
FileVisitOption, FileVisitResult} |
|
78169
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
15 |
import java.nio.file.attribute.{BasicFileAttributes, PosixFilePermission} |
75701 | 16 |
import java.net.{URI, 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} |
69293
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
18 |
import java.util.EnumSet |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
19 |
|
76353 | 20 |
import org.tukaani.xz |
21 |
import com.github.luben.zstd |
|
76348 | 22 |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
23 |
import scala.collection.mutable |
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 |
|
75393 | 26 |
object File { |
60992 | 27 |
/* standard path (Cygwin or Posix) */ |
60988 | 28 |
|
29 |
def standard_path(path: Path): String = path.expand.implode |
|
30 |
||
60992 | 31 |
def standard_path(platform_path: String): String = |
73911 | 32 |
isabelle.setup.Environment.standard_path(platform_path) |
60992 | 33 |
|
34 |
def standard_path(file: JFile): String = standard_path(file.getPath) |
|
35 |
||
36 |
def standard_url(name: String): String = |
|
37 |
try { |
|
38 |
val url = new URL(name) |
|
64775 | 39 |
if (url.getProtocol == "file" && Url.is_wellformed_file(name)) |
40 |
standard_path(Url.parse_file(name)) |
|
60992 | 41 |
else name |
42 |
} |
|
43 |
catch { case _: MalformedURLException => standard_path(name) } |
|
44 |
||
45 |
||
46 |
/* platform path (Windows or Posix) */ |
|
47 |
||
48 |
def platform_path(standard_path: String): String = |
|
73911 | 49 |
isabelle.setup.Environment.platform_path(standard_path) |
60992 | 50 |
|
51 |
def platform_path(path: Path): String = platform_path(standard_path(path)) |
|
60988 | 52 |
def platform_file(path: Path): JFile = new JFile(platform_path(path)) |
53 |
||
60992 | 54 |
|
76884 | 55 |
/* symbolic path representation, e.g. "~~/src/Pure/ROOT.ML" */ |
56 |
||
57 |
def symbolic_path(path: Path): String = { |
|
77218 | 58 |
val directories = space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse |
76884 | 59 |
val full_name = standard_path(path) |
60 |
directories.view.flatMap(a => |
|
61 |
try { |
|
62 |
val b = standard_path(Path.explode(a)) |
|
63 |
if (full_name == b) Some(a) |
|
64 |
else { |
|
65 |
Library.try_unprefix(b + "/", full_name) match { |
|
66 |
case Some(name) => Some(a + "/" + name) |
|
67 |
case None => None |
|
68 |
} |
|
69 |
} |
|
70 |
} catch { case ERROR(_) => None }).headOption.getOrElse(path.implode) |
|
71 |
} |
|
72 |
||
73 |
||
66232 | 74 |
/* platform files */ |
75 |
||
76 |
def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile |
|
77 |
def canonical(file: JFile): JFile = file.getCanonicalFile |
|
78 |
||
79 |
def path(file: JFile): Path = Path.explode(standard_path(file)) |
|
76546 | 80 |
def path(java_path: JPath): Path = path(java_path.toFile) |
81 |
||
66232 | 82 |
def pwd(): Path = path(Path.current.absolute_file) |
83 |
||
75701 | 84 |
def uri(file: JFile): URI = file.toURI |
85 |
def uri(path: Path): URI = path.file.toURI |
|
86 |
||
87 |
def url(file: JFile): URL = uri(file).toURL |
|
88 |
def url(path: Path): URL = url(path.file) |
|
89 |
||
66232 | 90 |
|
75906
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
91 |
/* adhoc file types */ |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
92 |
|
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
93 |
def is_ML(s: String): Boolean = s.endsWith(".ML") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
94 |
def is_bib(s: String): Boolean = s.endsWith(".bib") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
95 |
def is_dll(s: String): Boolean = s.endsWith(".dll") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
96 |
def is_exe(s: String): Boolean = s.endsWith(".exe") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
97 |
def is_gz(s: String): Boolean = s.endsWith(".gz") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
98 |
def is_html(s: String): Boolean = s.endsWith(".html") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
99 |
def is_jar(s: String): Boolean = s.endsWith(".jar") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
100 |
def is_java(s: String): Boolean = s.endsWith(".java") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
101 |
def is_node(s: String): Boolean = s.endsWith(".node") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
102 |
def is_pdf(s: String): Boolean = s.endsWith(".pdf") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
103 |
def is_png(s: String): Boolean = s.endsWith(".png") |
76540
83de6e9ae983
clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents:
76533
diff
changeset
|
104 |
def is_tar_bz2(s: String): Boolean = s.endsWith(".tar.bz2") |
76533 | 105 |
def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz") |
76540
83de6e9ae983
clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents:
76533
diff
changeset
|
106 |
def is_tgz(s: String): Boolean = s.endsWith(".tgz") |
75906
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
107 |
def is_thy(s: String): Boolean = s.endsWith(".thy") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
108 |
def is_xz(s: String): Boolean = s.endsWith(".xz") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
109 |
def is_zip(s: String): Boolean = s.endsWith(".zip") |
76348 | 110 |
def is_zst(s: String): Boolean = s.endsWith(".zst") |
75906
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
111 |
|
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
112 |
def is_backup(s: String): Boolean = s.endsWith("~") || s.endsWith(".orig") |
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
113 |
|
2167b9e3157a
clarified signature: support for adhoc file types;
wenzelm
parents:
75825
diff
changeset
|
114 |
|
66693 | 115 |
/* relative paths */ |
116 |
||
75393 | 117 |
def relative_path(base: Path, other: Path): Option[Path] = { |
73945 | 118 |
val base_path = base.java_path |
119 |
val other_path = other.java_path |
|
66693 | 120 |
if (other_path.startsWith(base_path)) |
121 |
Some(path(base_path.relativize(other_path).toFile)) |
|
122 |
else None |
|
123 |
} |
|
124 |
||
125 |
||
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 |
/* bash path */ |
60992 | 127 |
|
64304 | 128 |
def bash_path(path: Path): String = Bash.string(standard_path(path)) |
129 |
def bash_path(file: JFile): String = Bash.string(standard_path(file)) |
|
60988 | 130 |
|
72036 | 131 |
def bash_platform_path(path: Path): String = Bash.string(platform_path(path)) |
132 |
||
60988 | 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 |
||
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
143 |
/* directory content */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
144 |
|
75393 | 145 |
def read_dir(dir: Path): List[String] = { |
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
|
146 |
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
|
147 |
val files = dir.file.listFiles |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
148 |
if (files == null) Nil |
69427
ff2f39a221d4
clarified operations: uniform sorting of results;
wenzelm
parents:
69405
diff
changeset
|
149 |
else files.toList.map(_.getName).sorted |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62704
diff
changeset
|
150 |
} |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
151 |
|
76529 | 152 |
def get_entry( |
153 |
dir: Path, |
|
154 |
pred: Path => Boolean = _ => true, |
|
155 |
title: String = "" |
|
156 |
): Path = |
|
157 |
read_dir(dir).filter(name => pred(dir + Path.basic(name))) match { |
|
158 |
case List(entry) => dir + Path.basic(entry) |
|
159 |
case bad => |
|
160 |
error("Bad directory content in " + (if (title.nonEmpty) title else dir.toString) + |
|
161 |
"\nexpected a single entry, but found" + |
|
162 |
(if (bad.isEmpty) " nothing" |
|
163 |
else bad.sorted.map(quote).mkString(":\n ", "\n ", ""))) |
|
72442 | 164 |
} |
165 |
||
76529 | 166 |
def get_file(dir: Path, title: String = ""): Path = |
167 |
get_entry(dir, pred = _.is_file, title = title) |
|
168 |
||
169 |
def get_dir(dir: Path, title: String = ""): Path = |
|
170 |
get_entry(dir, pred = _.is_dir, title = title) |
|
171 |
||
64932 | 172 |
def find_files( |
173 |
start: JFile, |
|
174 |
pred: JFile => Boolean = _ => true, |
|
69293
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
175 |
include_dirs: Boolean = false, |
75393 | 176 |
follow_links: Boolean = false |
177 |
): List[JFile] = { |
|
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
178 |
val result = new mutable.ListBuffer[JFile] |
73340 | 179 |
def check(file: JFile): Unit = if (pred(file)) result += file |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
180 |
|
64932 | 181 |
if (start.isFile) check(start) |
62443
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
182 |
else if (start.isDirectory) { |
69293
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
183 |
val options = |
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
184 |
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
|
185 |
else EnumSet.noneOf(classOf[FileVisitOption]) |
72a9860f8602
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
wenzelm
parents:
66693
diff
changeset
|
186 |
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
|
187 |
new SimpleFileVisitor[JPath] { |
75393 | 188 |
override def preVisitDirectory( |
189 |
path: JPath, |
|
190 |
attrs: BasicFileAttributes |
|
191 |
): FileVisitResult = { |
|
64932 | 192 |
if (include_dirs) check(path.toFile) |
193 |
FileVisitResult.CONTINUE |
|
194 |
} |
|
75393 | 195 |
override def visitFile( |
196 |
path: JPath, |
|
197 |
attrs: BasicFileAttributes |
|
198 |
): FileVisitResult = { |
|
69301 | 199 |
val file = path.toFile |
200 |
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
|
201 |
FileVisitResult.CONTINUE |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
202 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
203 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
204 |
) |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
205 |
} |
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
206 |
|
133f65ac17e5
just one File.find_files, based on Java 7 Files operations;
wenzelm
parents:
62294
diff
changeset
|
207 |
result.toList |
48613
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
208 |
} |
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
209 |
|
232652ac346e
clarified directory content operations (similar to ML version);
wenzelm
parents:
48550
diff
changeset
|
210 |
|
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
211 |
/* read */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
212 |
|
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
|
213 |
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
|
214 |
def read(path: Path): String = read(path.file) |
f686cb016c0c
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
wenzelm
parents:
48613
diff
changeset
|
215 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
216 |
|
75393 | 217 |
def read_stream(reader: BufferedReader): String = { |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
218 |
val output = new StringBuilder(100) |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
219 |
var c = -1 |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
220 |
while ({ c = reader.read; c != -1 }) output += c.toChar |
73367 | 221 |
reader.close() |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
222 |
output.toString |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
223 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
224 |
|
50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
225 |
def read_stream(stream: InputStream): String = |
64000 | 226 |
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
|
227 |
|
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
228 |
def read_gzip(file: JFile): String = |
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50203
diff
changeset
|
229 |
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) |
64000 | 230 |
def read_gzip(path: Path): String = read_gzip(path.file) |
51504 | 231 |
|
64002 | 232 |
def read_xz(file: JFile): String = |
76353 | 233 |
read_stream(new xz.XZInputStream(new BufferedInputStream(new FileInputStream(file)))) |
64000 | 234 |
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
|
235 |
|
76348 | 236 |
def read_zstd(file: JFile): String = { |
76349
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
237 |
Zstd.init() |
76353 | 238 |
read_stream(new zstd.ZstdInputStream(new BufferedInputStream(new FileInputStream(file)))) |
76348 | 239 |
} |
240 |
def read_zstd(path: Path): String = read_zstd(path.file) |
|
241 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
242 |
|
50845 | 243 |
/* read lines */ |
244 |
||
75393 | 245 |
def read_line(reader: BufferedReader): Option[String] = { |
69487 | 246 |
val line = |
247 |
try { reader.readLine} |
|
248 |
catch { case _: IOException => null } |
|
72698 | 249 |
Option(line).map(Library.trim_line) |
69487 | 250 |
} |
251 |
||
75393 | 252 |
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = { |
50845 | 253 |
val result = new mutable.ListBuffer[String] |
69487 | 254 |
var line: Option[String] = None |
255 |
while ({ line = read_line(reader); line.isDefined }) { |
|
256 |
progress(line.get) |
|
257 |
result += line.get |
|
50845 | 258 |
} |
73367 | 259 |
reader.close() |
50845 | 260 |
result.toList |
261 |
} |
|
262 |
||
263 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
264 |
/* write */ |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
265 |
|
71534 | 266 |
def writer(file: JFile): BufferedWriter = |
267 |
new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset)) |
|
268 |
||
73340 | 269 |
def write_file( |
75393 | 270 |
file: JFile, |
271 |
text: String, |
|
272 |
make_stream: OutputStream => OutputStream |
|
273 |
): Unit = { |
|
51504 | 274 |
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
|
275 |
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
|
276 |
} |
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
277 |
|
73574
12b3f78dde61
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents:
73367
diff
changeset
|
278 |
def write(file: JFile, text: String): Unit = write_file(file, text, s => s) |
12b3f78dde61
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents:
73367
diff
changeset
|
279 |
def write(path: Path, text: String): Unit = write(path.file, text) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
280 |
|
73574
12b3f78dde61
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents:
73367
diff
changeset
|
281 |
def write_gzip(file: JFile, text: String): Unit = |
51504 | 282 |
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) |
73574
12b3f78dde61
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents:
73367
diff
changeset
|
283 |
def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
284 |
|
76351
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
285 |
def write_xz(file: JFile, text: String, options: Compress.Options_XZ): Unit = |
76353 | 286 |
File.write_file(file, text, |
287 |
s => new xz.XZOutputStream(new BufferedOutputStream(s), options.make)) |
|
76351
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
288 |
def write_xz(file: JFile, text: String): Unit = write_xz(file, text, Compress.Options_XZ()) |
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
289 |
def write_xz(path: Path, text: String, options: Compress.Options_XZ): Unit = |
64002 | 290 |
write_xz(path.file, text, options) |
76351
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
291 |
def write_xz(path: Path, text: String): Unit = write_xz(path, text, Compress.Options_XZ()) |
64000 | 292 |
|
76351
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
293 |
def write_zstd(file: JFile, text: String, options: Compress.Options_Zstd): Unit = { |
76349
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
294 |
Zstd.init() |
76353 | 295 |
File.write_file(file, text, |
296 |
s => new zstd.ZstdOutputStream(new BufferedOutputStream(s), options.level)) |
|
76348 | 297 |
} |
76351
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
298 |
def write_zstd(file: JFile, text: String): Unit = |
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
299 |
write_zstd(file, text, Compress.Options_Zstd()) |
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
300 |
def write_zstd(path: Path, text: String, options: Compress.Options_Zstd): Unit = |
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
301 |
write_zstd(path.file, text, options) |
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
302 |
def write_zstd(path: Path, text: String): Unit = |
2cee31cd92f0
generic support for XZ and Zstd compression in Isabelle/Scala;
wenzelm
parents:
76349
diff
changeset
|
303 |
write_zstd(path, text, Compress.Options_Zstd()) |
76348 | 304 |
|
75393 | 305 |
def write_backup(path: Path, text: String): Unit = { |
73317 | 306 |
if (path.is_file) Isabelle_System.move_file(path, path.backup) |
62444 | 307 |
write(path, text) |
53336 | 308 |
} |
309 |
||
75393 | 310 |
def write_backup2(path: Path, text: String): Unit = { |
73317 | 311 |
if (path.is_file) Isabelle_System.move_file(path, path.backup2) |
62444 | 312 |
write(path, text) |
58610 | 313 |
} |
314 |
||
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
315 |
|
62703 | 316 |
/* append */ |
317 |
||
73574
12b3f78dde61
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents:
73367
diff
changeset
|
318 |
def append(file: JFile, text: String): Unit = |
73627 | 319 |
Files.write(file.toPath, UTF8.bytes(text), |
62703 | 320 |
StandardOpenOption.APPEND, StandardOpenOption.CREATE) |
321 |
||
73574
12b3f78dde61
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
wenzelm
parents:
73367
diff
changeset
|
322 |
def append(path: Path, text: String): Unit = append(path.file, text) |
62703 | 323 |
|
324 |
||
75206 | 325 |
/* change */ |
326 |
||
75393 | 327 |
def change( |
328 |
path: Path, |
|
329 |
init: Boolean = false, |
|
330 |
strict: Boolean = false |
|
331 |
)(f: String => String): Unit = { |
|
75208 | 332 |
if (!path.is_file && init) write(path, "") |
75206 | 333 |
val x = read(path) |
334 |
val y = f(x) |
|
335 |
if (x != y) write(path, y) |
|
75213 | 336 |
else if (strict) error("Unchanged file: " + path) |
75206 | 337 |
} |
338 |
||
75213 | 339 |
def change_lines(path: Path, init: Boolean = false, strict: Boolean = false)( |
340 |
f: List[String] => List[String]): Unit = |
|
341 |
change(path, init = init, strict = strict)(text => cat_lines(f(split_lines(text)))) |
|
75206 | 342 |
|
343 |
||
64213 | 344 |
/* eq */ |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
345 |
|
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
346 |
def eq(file1: JFile, file2: JFile): Boolean = |
73318 | 347 |
try { Files.isSameFile(file1.toPath, file2.toPath) } |
49673
2a088cff1e7b
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
wenzelm
parents:
49610
diff
changeset
|
348 |
catch { case ERROR(_) => false } |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
349 |
|
64213 | 350 |
def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) |
351 |
||
352 |
||
64934 | 353 |
/* eq_content */ |
354 |
||
355 |
def eq_content(file1: JFile, file2: JFile): Boolean = |
|
356 |
if (eq(file1, file2)) true |
|
357 |
else if (file1.length != file2.length) false |
|
358 |
else Bytes.read(file1) == Bytes.read(file2) |
|
359 |
||
360 |
def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) |
|
361 |
||
362 |
||
69405
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
363 |
/* permissions */ |
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
364 |
|
78169
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
365 |
private val restrict_perms: List[PosixFilePermission] = |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
366 |
List( |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
367 |
PosixFilePermission.GROUP_READ, |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
368 |
PosixFilePermission.GROUP_WRITE, |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
369 |
PosixFilePermission.GROUP_EXECUTE, |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
370 |
PosixFilePermission.OTHERS_READ, |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
371 |
PosixFilePermission.OTHERS_WRITE, |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
372 |
PosixFilePermission.OTHERS_EXECUTE) |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
373 |
|
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
374 |
def restrict(path: Path): Unit = |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
375 |
if (Platform.is_windows) Isabelle_System.chmod("g-rwx,o-rwx", path) |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
376 |
else { |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
377 |
val perms = Files.getPosixFilePermissions(path.java_path) |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
378 |
var perms_changed = false |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
379 |
for (p <- restrict_perms if perms.contains(p)) { |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
380 |
perms.remove(p) |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
381 |
perms_changed = true |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
382 |
} |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
383 |
if (perms_changed) Files.setPosixFilePermissions(path.java_path, perms) |
5ad1ae8626de
minor performance tuning: avoid external process;
wenzelm
parents:
78161
diff
changeset
|
384 |
} |
78161 | 385 |
|
75393 | 386 |
def is_executable(path: Path): Boolean = { |
69788 | 387 |
if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok |
388 |
else path.file.canExecute |
|
389 |
} |
|
390 |
||
78158 | 391 |
def set_executable(path: Path, flag: Boolean = false): Unit = { |
71114 | 392 |
if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) |
393 |
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
|
394 |
else path.file.setExecutable(flag, false) |
69405
22428643351f
more direct File.executable operation: avoid external process (on Unix);
wenzelm
parents:
69402
diff
changeset
|
395 |
} |
74811 | 396 |
|
397 |
||
398 |
/* content */ |
|
399 |
||
75825 | 400 |
def content(path: Path, content: Bytes): Content = new Content(path, content) |
401 |
def content(path: Path, content: String): Content = new Content(path, Bytes(content)) |
|
75824 | 402 |
def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) |
74811 | 403 |
|
75825 | 404 |
final class Content private[File](val path: Path, val content: Bytes) { |
75677 | 405 |
override def toString: String = path.toString |
74811 | 406 |
|
77852
df35b5b7b6a4
more direct hg_sync init via ssh (see also 721b3278c8e4);
wenzelm
parents:
77218
diff
changeset
|
407 |
def write(dir: Path, ssh: SSH.System = SSH.Local): Unit = { |
75508 | 408 |
val full_path = dir + path |
77852
df35b5b7b6a4
more direct hg_sync init via ssh (see also 721b3278c8e4);
wenzelm
parents:
77218
diff
changeset
|
409 |
ssh.make_directory(ssh.expand_path(full_path).dir) |
df35b5b7b6a4
more direct hg_sync init via ssh (see also 721b3278c8e4);
wenzelm
parents:
77218
diff
changeset
|
410 |
ssh.write_bytes(full_path, content) |
75508 | 411 |
} |
74811 | 412 |
} |
413 |
||
75676 | 414 |
final class Content_XML private[File](val path: Path, val content: XML.Body) { |
75823
6eb8d6cdb686
proper toString for Content_XML, which is not covered by trait Content;
wenzelm
parents:
75701
diff
changeset
|
415 |
override def toString: String = path.toString |
6eb8d6cdb686
proper toString for Content_XML, which is not covered by trait Content;
wenzelm
parents:
75701
diff
changeset
|
416 |
|
75825 | 417 |
def output(out: XML.Body => String): Content = new Content(path, Bytes(out(content))) |
74811 | 418 |
} |
77109
e3a2b3536030
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
wenzelm
parents:
76884
diff
changeset
|
419 |
|
e3a2b3536030
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
wenzelm
parents:
76884
diff
changeset
|
420 |
|
e3a2b3536030
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
wenzelm
parents:
76884
diff
changeset
|
421 |
/* space */ |
e3a2b3536030
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
wenzelm
parents:
76884
diff
changeset
|
422 |
|
e3a2b3536030
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
wenzelm
parents:
76884
diff
changeset
|
423 |
def space(path: Path): Space = |
77110
595358b9f61d
prefer strict operation: java.io.File.length returns 0 for non-existent file;
wenzelm
parents:
77109
diff
changeset
|
424 |
Space.bytes(check_file(path).file.length) |
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
diff
changeset
|
425 |
} |