8 sig |
8 sig |
9 val isabelle_tool: string -> string -> int |
9 val isabelle_tool: string -> string -> int |
10 val mkdirs: Path.T -> unit |
10 val mkdirs: Path.T -> unit |
11 val mkdir: Path.T -> unit |
11 val mkdir: Path.T -> unit |
12 val copy_dir: Path.T -> Path.T -> unit |
12 val copy_dir: Path.T -> Path.T -> unit |
|
13 val copy_file: Path.T -> Path.T -> unit |
|
14 val copy_file_base: Path.T * Path.T -> Path.T -> unit |
13 val create_tmp_path: string -> string -> Path.T |
15 val create_tmp_path: string -> string -> Path.T |
14 val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
16 val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
15 val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
17 val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
16 val with_tmp_fifo: (Path.T -> 'a) -> 'a |
18 val with_tmp_fifo: (Path.T -> 'a) -> 'a |
17 val bash_output: string -> string * int |
19 val bash_output: string -> string * int |
64 |
66 |
65 fun copy_dir src dst = |
67 fun copy_dir src dst = |
66 if File.eq (src, dst) then () |
68 if File.eq (src, dst) then () |
67 else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ()); |
69 else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ()); |
68 |
70 |
|
71 fun copy_file src0 dst0 = |
|
72 let |
|
73 val src = Path.expand src0; |
|
74 val dst = Path.expand dst0; |
|
75 val (target_dir, target) = |
|
76 if File.is_dir dst then (dst, Path.append dst (Path.base src)) |
|
77 else (Path.dir dst, dst); |
|
78 in |
|
79 if File.eq (src, target) then () |
|
80 else |
|
81 (ignore o system_command) |
|
82 ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target_dir ^ "/.") |
|
83 end; |
|
84 |
|
85 fun copy_file_base (base_dir, src0) target_dir = |
|
86 let |
|
87 val src = Path.expand src0; |
|
88 val src_dir = Path.dir src; |
|
89 val _ = |
|
90 if Path.starts_basic src then () |
|
91 else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); |
|
92 val _ = mkdirs (Path.append target_dir src_dir); |
|
93 in copy_file (Path.append base_dir src) (Path.append target_dir src) end; |
|
94 |
69 |
95 |
70 (* tmp files *) |
96 (* tmp files *) |
71 |
97 |
72 fun create_tmp_path name ext = |
98 fun create_tmp_path name ext = |
73 let |
99 let |