--- a/src/Pure/General/file.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Pure/General/file.ML Sat Nov 27 15:28:00 2010 +0100
@@ -13,13 +13,9 @@
val pwd: unit -> Path.T
val full_path: Path.T -> Path.T
val tmp_path: Path.T -> Path.T
- val isabelle_tool: string -> string -> int
val exists: Path.T -> bool
val check: Path.T -> unit
val rm: Path.T -> unit
- val rm_tree: Path.T -> unit
- val mkdir: Path.T -> unit
- val mkdir_leaf: Path.T -> unit
val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -32,7 +28,6 @@
val write_buffer: Path.T -> Buffer.T -> unit
val eq: Path.T * Path.T -> bool
val copy: Path.T -> Path.T -> unit
- val copy_dir: Path.T -> Path.T -> unit
end;
structure File: FILE =
@@ -62,25 +57,6 @@
Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
-(* system commands *)
-
-fun isabelle_tool name args =
- (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
- let val path = dir ^ "/" ^ name in
- if can OS.FileSys.modTime path andalso
- not (OS.FileSys.isDir path) andalso
- OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
- then SOME path
- else NONE
- end handle OS.SysErr _ => NONE) of
- SOME path => bash (shell_quote path ^ " " ^ args)
- | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
-
-fun system_command cmd =
- if bash cmd <> 0 then error ("System command failed: " ^ cmd)
- else ();
-
-
(* directory entries *)
val exists = can OS.FileSys.modTime o platform_path;
@@ -91,12 +67,6 @@
val rm = OS.FileSys.remove o platform_path;
-fun rm_tree path = system_command ("rm -r " ^ shell_path path);
-
-fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
-
-fun mkdir_leaf path = (check (Path.dir path); mkdir path);
-
fun is_dir path =
the_default false (try OS.FileSys.isDir (platform_path path));
@@ -163,8 +133,4 @@
let val target = if is_dir dst then Path.append dst (Path.base src) else dst
in write target (read src) end;
-fun copy_dir src dst =
- if eq (src, dst) then ()
- else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
-
end;