40743
|
1 |
(* Title: Pure/System/isabelle_system.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Isabelle system support.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature ISABELLE_SYSTEM =
|
|
8 |
sig
|
|
9 |
val isabelle_tool: string -> string -> int
|
|
10 |
val rm_tree: Path.T -> unit
|
|
11 |
val mkdirs: Path.T -> unit
|
|
12 |
val mkdir_leaf: Path.T -> unit
|
|
13 |
val copy_dir: Path.T -> Path.T -> unit
|
|
14 |
end;
|
|
15 |
|
|
16 |
structure Isabelle_System: ISABELLE_SYSTEM =
|
|
17 |
struct
|
|
18 |
|
|
19 |
(* system commands *)
|
|
20 |
|
|
21 |
fun isabelle_tool name args =
|
|
22 |
(case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
|
|
23 |
let val path = dir ^ "/" ^ name in
|
|
24 |
if can OS.FileSys.modTime path andalso
|
|
25 |
not (OS.FileSys.isDir path) andalso
|
|
26 |
OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
|
|
27 |
then SOME path
|
|
28 |
else NONE
|
|
29 |
end handle OS.SysErr _ => NONE) of
|
|
30 |
SOME path => bash (File.shell_quote path ^ " " ^ args)
|
|
31 |
| NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
|
|
32 |
|
|
33 |
fun system_command cmd =
|
|
34 |
if bash cmd <> 0 then error ("System command failed: " ^ cmd)
|
|
35 |
else ();
|
|
36 |
|
|
37 |
|
|
38 |
(* directory operations *)
|
|
39 |
|
|
40 |
fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
|
|
41 |
|
|
42 |
fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
|
|
43 |
|
|
44 |
fun mkdir_leaf path = (File.check (Path.dir path); mkdirs path); (* FIXME ? *)
|
|
45 |
|
|
46 |
fun copy_dir src dst =
|
|
47 |
if File.eq (src, dst) then ()
|
|
48 |
else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
|
|
49 |
|
|
50 |
end;
|
|
51 |
|