author | wenzelm |
Thu, 10 Oct 2024 14:13:18 +0200 | |
changeset 81146 | 87f173836d56 |
parent 77180 | 7af930cd0fce |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/file.ML |
64698 | 2 |
Author: Makarius |
5009 | 3 |
|
64698 | 4 |
File-system operations. |
5009 | 5 |
*) |
6 |
||
7 |
signature FILE = |
|
8 |
sig |
|
60970
e08d868ceca9
clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
wenzelm
parents:
59058
diff
changeset
|
9 |
val standard_path: Path.T -> string |
16261 | 10 |
val platform_path: Path.T -> string |
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62468
diff
changeset
|
11 |
val bash_path: Path.T -> string |
69223 | 12 |
val bash_paths: Path.T list -> string |
72278 | 13 |
val bash_platform_path: Path.T -> string |
76884 | 14 |
val symbolic_path: Path.T -> string |
73314
87403fde8cc3
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents:
73264
diff
changeset
|
15 |
val absolute_path: Path.T -> Path.T |
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
16 |
val full_path: Path.T -> Path.T -> Path.T |
6182 | 17 |
val tmp_path: Path.T -> Path.T |
17826 | 18 |
val exists: Path.T -> bool |
19 |
val rm: Path.T -> unit |
|
40785 | 20 |
val is_dir: Path.T -> bool |
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
21 |
val is_file: Path.T -> bool |
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
22 |
val check_dir: Path.T -> Path.T |
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
23 |
val check_file: Path.T -> Path.T |
43848 | 24 |
val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a |
25 |
val read_dir: Path.T -> string list |
|
75616
986506233812
clarified signature: File.read_lines is based on scalable Bytes.T;
wenzelm
parents:
75615
diff
changeset
|
26 |
val read: Path.T -> string |
43848 | 27 |
val read_lines: Path.T -> string list |
6182 | 28 |
val write: Path.T -> string -> unit |
29 |
val append: Path.T -> string -> unit |
|
16713 | 30 |
val write_list: Path.T -> string list -> unit |
31 |
val append_list: Path.T -> string list -> unit |
|
16603 | 32 |
val eq: Path.T * Path.T -> bool |
5009 | 33 |
end; |
34 |
||
35 |
structure File: FILE = |
|
36 |
struct |
|
37 |
||
26503
4dec4460244f
discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents:
26220
diff
changeset
|
38 |
(* system path representations *) |
6224 | 39 |
|
60970
e08d868ceca9
clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
wenzelm
parents:
59058
diff
changeset
|
40 |
val standard_path = Path.implode o Path.expand; |
62468 | 41 |
val platform_path = ML_System.platform_path o standard_path; |
26980
f7f48bb9a025
ident: naive caching prevents potentially slow external invocations;
wenzelm
parents:
26946
diff
changeset
|
42 |
|
73264 | 43 |
val bash_path = Bash.string o standard_path; |
44 |
val bash_paths = Bash.strings o map standard_path; |
|
6224 | 45 |
|
73264 | 46 |
val bash_platform_path = Bash.string o platform_path; |
72278 | 47 |
|
70292 | 48 |
|
76884 | 49 |
(* symbolic path representation, e.g. "~~/src/Pure/ROOT.ML" *) |
50 |
||
51 |
fun symbolic_path path = |
|
52 |
let |
|
53 |
val directories = rev (space_explode ":" (getenv "ISABELLE_DIRECTORIES")); |
|
54 |
val full_name = standard_path path; |
|
55 |
fun fold_path a = |
|
56 |
(case try (standard_path o Path.explode) a of |
|
57 |
SOME b => |
|
58 |
if full_name = b then SOME a |
|
59 |
else |
|
60 |
(case try (unprefix (b ^ "/")) full_name of |
|
61 |
SOME name => SOME (a ^ "/" ^ name) |
|
62 |
| NONE => NONE) |
|
63 |
| NONE => NONE); |
|
64 |
in |
|
65 |
(case get_first fold_path directories of |
|
66 |
SOME name => name |
|
67 |
| NONE => Path.implode path) |
|
68 |
end; |
|
69 |
||
70 |
||
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
71 |
(* full_path *) |
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
72 |
|
73314
87403fde8cc3
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents:
73264
diff
changeset
|
73 |
val absolute_path = |
87403fde8cc3
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents:
73264
diff
changeset
|
74 |
Path.expand #> (fn path => |
87403fde8cc3
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents:
73264
diff
changeset
|
75 |
if Path.is_absolute path then path |
87403fde8cc3
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents:
73264
diff
changeset
|
76 |
else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path); |
87403fde8cc3
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents:
73264
diff
changeset
|
77 |
|
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
78 |
fun full_path dir path = |
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
79 |
let |
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
80 |
val path' = Path.expand path; |
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
81 |
val _ = Path.is_current path' andalso error "Bad file specification"; |
73314
87403fde8cc3
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents:
73264
diff
changeset
|
82 |
in absolute_path (dir + path') end; |
5009 | 83 |
|
6182 | 84 |
|
85 |
(* tmp_path *) |
|
86 |
||
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72278
diff
changeset
|
87 |
fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path; |
5009 | 88 |
|
89 |
||
26980
f7f48bb9a025
ident: naive caching prevents potentially slow external invocations;
wenzelm
parents:
26946
diff
changeset
|
90 |
(* directory entries *) |
f7f48bb9a025
ident: naive caching prevents potentially slow external invocations;
wenzelm
parents:
26946
diff
changeset
|
91 |
|
77180
7af930cd0fce
more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);
wenzelm
parents:
76884
diff
changeset
|
92 |
val exists = can OS.FileSys.fileId o platform_path; |
16261 | 93 |
|
94 |
val rm = OS.FileSys.remove o platform_path; |
|
95 |
||
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
96 |
fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path)); |
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
97 |
fun is_dir path = exists path andalso test_dir path; |
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
98 |
fun is_file path = exists path andalso not (test_dir path); |
40785 | 99 |
|
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
100 |
fun check_dir path = |
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
101 |
if is_dir path then path |
63668 | 102 |
else error ("No such directory: " ^ Path.print (Path.expand path)); |
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
103 |
|
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
104 |
fun check_file path = |
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
105 |
if is_file path then path |
63668 | 106 |
else error ("No such file: " ^ Path.print (Path.expand path)); |
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
107 |
|
16261 | 108 |
|
43848 | 109 |
(* directory content *) |
110 |
||
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
111 |
fun fold_dir f path a = |
75615 | 112 |
check_dir path |> File_Stream.open_dir (fn stream => |
69300
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
113 |
let |
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
114 |
fun read x = |
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
115 |
(case OS.FileSys.readDir stream of |
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
116 |
NONE => x |
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
117 |
| SOME entry => read (f entry x)); |
8b6ab9989bcd
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents:
69223
diff
changeset
|
118 |
in read a end); |
43848 | 119 |
|
69427
ff2f39a221d4
clarified operations: uniform sorting of results;
wenzelm
parents:
69300
diff
changeset
|
120 |
fun read_dir path = sort_strings (fold_dir cons path []); |
43848 | 121 |
|
122 |
||
75616
986506233812
clarified signature: File.read_lines is based on scalable Bytes.T;
wenzelm
parents:
75615
diff
changeset
|
123 |
(* read *) |
43848 | 124 |
|
75615 | 125 |
val read = File_Stream.open_input File_Stream.input_all; |
5009 | 126 |
|
75616
986506233812
clarified signature: File.read_lines is based on scalable Bytes.T;
wenzelm
parents:
75615
diff
changeset
|
127 |
val read_lines = Bytes.read #> Bytes.trim_split_lines; |
986506233812
clarified signature: File.read_lines is based on scalable Bytes.T;
wenzelm
parents:
75615
diff
changeset
|
128 |
|
28028 | 129 |
|
75615 | 130 |
(* write *) |
28028 | 131 |
|
75615 | 132 |
fun write_list path ss = File_Stream.open_output (fn stream => File_Stream.outputs stream ss) path; |
133 |
fun append_list path ss = File_Stream.open_append (fn stream => File_Stream.outputs stream ss) path; |
|
16713 | 134 |
|
135 |
fun write path txt = write_list path [txt]; |
|
136 |
fun append path txt = append_list path [txt]; |
|
6182 | 137 |
|
28028 | 138 |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
48911
diff
changeset
|
139 |
(* eq *) |
5009 | 140 |
|
16603 | 141 |
fun eq paths = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
56533
diff
changeset
|
142 |
(case try (apply2 (OS.FileSys.fileId o platform_path)) paths of |
26656 | 143 |
SOME ids => is_equal (OS.FileSys.compare ids) |
16603 | 144 |
| NONE => false); |
145 |
||
5009 | 146 |
end; |