src/Pure/System/isabelle_system.ML
author wenzelm
Mon Dec 20 14:44:00 2010 +0100 (2010-12-20)
changeset 41307 bb8468ae414e
parent 40785 c755df0f7062
child 41352 87adb55fb0fb
permissions -rw-r--r--
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
more robust rm_tree -- somewhat dangerous and not exported;
tuned;
wenzelm@40743
     1
(*  Title:      Pure/System/isabelle_system.ML
wenzelm@40743
     2
    Author:     Makarius
wenzelm@40743
     3
wenzelm@40743
     4
Isabelle system support.
wenzelm@40743
     5
*)
wenzelm@40743
     6
wenzelm@40743
     7
signature ISABELLE_SYSTEM =
wenzelm@40743
     8
sig
wenzelm@40743
     9
  val isabelle_tool: string -> string -> int
wenzelm@40743
    10
  val mkdirs: Path.T -> unit
wenzelm@40745
    11
  val mkdir: Path.T -> unit
wenzelm@40743
    12
  val copy_dir: Path.T -> Path.T -> unit
wenzelm@41307
    13
  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
wenzelm@41307
    14
  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
wenzelm@40743
    15
end;
wenzelm@40743
    16
wenzelm@40743
    17
structure Isabelle_System: ISABELLE_SYSTEM =
wenzelm@40743
    18
struct
wenzelm@40743
    19
wenzelm@40743
    20
(* system commands *)
wenzelm@40743
    21
wenzelm@40743
    22
fun isabelle_tool name args =
wenzelm@40743
    23
  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
wenzelm@40743
    24
      let val path = dir ^ "/" ^ name in
wenzelm@40743
    25
        if can OS.FileSys.modTime path andalso
wenzelm@40743
    26
          not (OS.FileSys.isDir path) andalso
wenzelm@40743
    27
          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
wenzelm@40743
    28
        then SOME path
wenzelm@40743
    29
        else NONE
wenzelm@40743
    30
      end handle OS.SysErr _ => NONE) of
wenzelm@40743
    31
    SOME path => bash (File.shell_quote path ^ " " ^ args)
wenzelm@40743
    32
  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
wenzelm@40743
    33
wenzelm@40743
    34
fun system_command cmd =
wenzelm@40743
    35
  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
wenzelm@40743
    36
  else ();
wenzelm@40743
    37
wenzelm@40743
    38
wenzelm@40743
    39
(* directory operations *)
wenzelm@40743
    40
wenzelm@40743
    41
fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
wenzelm@40743
    42
wenzelm@40785
    43
fun mkdir path =
wenzelm@40785
    44
  if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
wenzelm@40743
    45
wenzelm@40743
    46
fun copy_dir src dst =
wenzelm@40743
    47
  if File.eq (src, dst) then ()
wenzelm@40743
    48
  else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
wenzelm@40743
    49
wenzelm@41307
    50
wenzelm@41307
    51
(* unique tmp files *)
wenzelm@41307
    52
wenzelm@41307
    53
local
wenzelm@41307
    54
wenzelm@41307
    55
fun fresh_path name =
wenzelm@41307
    56
  let
wenzelm@41307
    57
    val path = File.tmp_path (Path.basic (name ^ serial_string ()));
wenzelm@41307
    58
    val _ = File.exists path andalso
wenzelm@41307
    59
      raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
wenzelm@41307
    60
  in path end;
wenzelm@41307
    61
wenzelm@41307
    62
fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
wenzelm@41307
    63
wenzelm@41307
    64
in
wenzelm@41307
    65
wenzelm@41307
    66
fun with_tmp_file name f =
wenzelm@41307
    67
  let val path = fresh_path name
wenzelm@41307
    68
  in Exn.release (Exn.capture f path before try File.rm path) end;
wenzelm@41307
    69
wenzelm@41307
    70
fun with_tmp_dir name f =
wenzelm@41307
    71
  let
wenzelm@41307
    72
    val path = fresh_path name;
wenzelm@41307
    73
    val _ = mkdirs path;
wenzelm@41307
    74
  in Exn.release (Exn.capture f path before try rm_tree path) end;
wenzelm@41307
    75
wenzelm@40743
    76
end;
wenzelm@40743
    77
wenzelm@41307
    78
end;
wenzelm@41307
    79