src/Pure/System/isabelle_system.ML
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 50843 1465521b92a1
child 56498 6437c989a744
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
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@42127
    13
  val create_tmp_path: string -> string -> Path.T
wenzelm@42127
    14
  val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
wenzelm@41307
    15
  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
wenzelm@43849
    16
  val with_tmp_fifo: (Path.T -> 'a) -> 'a
wenzelm@43850
    17
  val bash_output: string -> string * int
wenzelm@43850
    18
  val bash: string -> int
wenzelm@40743
    19
end;
wenzelm@40743
    20
wenzelm@40743
    21
structure Isabelle_System: ISABELLE_SYSTEM =
wenzelm@40743
    22
struct
wenzelm@40743
    23
wenzelm@43850
    24
(* bash *)
wenzelm@43850
    25
wenzelm@43850
    26
fun bash_output s =
wenzelm@47499
    27
  let
wenzelm@47499
    28
    val {out, err, rc, ...} = Bash.process s;
wenzelm@47499
    29
    val _ = warning (trim_line err);
wenzelm@47499
    30
  in (out, rc) end;
wenzelm@43850
    31
wenzelm@43850
    32
fun bash s =
wenzelm@47499
    33
  let
wenzelm@47499
    34
    val (out, rc) = bash_output s;
wenzelm@47499
    35
    val _ = writeln (trim_line out);
wenzelm@47499
    36
  in rc end;
wenzelm@43850
    37
wenzelm@43850
    38
wenzelm@40743
    39
(* system commands *)
wenzelm@40743
    40
wenzelm@40743
    41
fun isabelle_tool name args =
wenzelm@40743
    42
  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
wenzelm@43606
    43
      let val path = File.platform_path (Path.append (Path.explode dir) (Path.basic name)) in
wenzelm@40743
    44
        if can OS.FileSys.modTime path andalso
wenzelm@40743
    45
          not (OS.FileSys.isDir path) andalso
wenzelm@40743
    46
          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
wenzelm@40743
    47
        then SOME path
wenzelm@40743
    48
        else NONE
wenzelm@40743
    49
      end handle OS.SysErr _ => NONE) of
wenzelm@40743
    50
    SOME path => bash (File.shell_quote path ^ " " ^ args)
wenzelm@47499
    51
  | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
wenzelm@40743
    52
wenzelm@40743
    53
fun system_command cmd =
wenzelm@40743
    54
  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
wenzelm@40743
    55
  else ();
wenzelm@40743
    56
wenzelm@40743
    57
wenzelm@40743
    58
(* directory operations *)
wenzelm@40743
    59
wenzelm@40743
    60
fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
wenzelm@40743
    61
wenzelm@40785
    62
fun mkdir path =
wenzelm@40785
    63
  if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
wenzelm@40743
    64
wenzelm@40743
    65
fun copy_dir src dst =
wenzelm@40743
    66
  if File.eq (src, dst) then ()
wenzelm@46502
    67
  else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
wenzelm@40743
    68
wenzelm@41307
    69
wenzelm@41307
    70
(* unique tmp files *)
wenzelm@41307
    71
wenzelm@42127
    72
fun create_tmp_path name ext =
wenzelm@41307
    73
  let
wenzelm@42127
    74
    val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext);
wenzelm@41307
    75
    val _ = File.exists path andalso
wenzelm@41944
    76
      raise Fail ("Temporary file already exists: " ^ Path.print path);
wenzelm@41307
    77
  in path end;
wenzelm@41307
    78
wenzelm@42127
    79
fun with_tmp_file name ext f =
wenzelm@42127
    80
  let val path = create_tmp_path name ext
wenzelm@42127
    81
  in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
wenzelm@41307
    82
wenzelm@42127
    83
fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
wenzelm@41307
    84
wenzelm@41307
    85
fun with_tmp_dir name f =
wenzelm@41307
    86
  let
wenzelm@42127
    87
    val path = create_tmp_path name "";
wenzelm@41307
    88
    val _ = mkdirs path;
wenzelm@41352
    89
  in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
wenzelm@41307
    90
wenzelm@43850
    91
wenzelm@43851
    92
(* fifo *)
wenzelm@43850
    93
wenzelm@43849
    94
fun with_tmp_fifo f =
wenzelm@43849
    95
  with_tmp_file "isabelle-fifo-" ""
wenzelm@43849
    96
    (fn path =>
wenzelm@43849
    97
      (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
wenzelm@43849
    98
        (_, 0) => f path
wenzelm@47499
    99
      | (out, _) => error (trim_line out)));
wenzelm@43849
   100
wenzelm@40743
   101
end;
wenzelm@40743
   102