src/Pure/System/isabelle_system.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 47499 4b0daca2bf88
child 50843 1465521b92a1
permissions -rw-r--r--
more official command specifications, including source position;
     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 mkdirs: Path.T -> unit
    11   val mkdir: Path.T -> unit
    12   val copy_dir: Path.T -> Path.T -> unit
    13   val create_tmp_path: string -> string -> Path.T
    14   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
    15   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
    16   val with_tmp_fifo: (Path.T -> 'a) -> 'a
    17   val bash_output_fifo: string -> (Path.T -> 'a) -> 'a
    18   val bash_output: string -> string * int
    19   val bash: string -> int
    20 end;
    21 
    22 structure Isabelle_System: ISABELLE_SYSTEM =
    23 struct
    24 
    25 (* bash *)
    26 
    27 fun bash_output s =
    28   let
    29     val {out, err, rc, ...} = Bash.process s;
    30     val _ = warning (trim_line err);
    31   in (out, rc) end;
    32 
    33 fun bash s =
    34   let
    35     val (out, rc) = bash_output s;
    36     val _ = writeln (trim_line out);
    37   in rc end;
    38 
    39 
    40 (* system commands *)
    41 
    42 fun isabelle_tool name args =
    43   (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
    44       let val path = File.platform_path (Path.append (Path.explode dir) (Path.basic name)) in
    45         if can OS.FileSys.modTime path andalso
    46           not (OS.FileSys.isDir path) andalso
    47           OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
    48         then SOME path
    49         else NONE
    50       end handle OS.SysErr _ => NONE) of
    51     SOME path => bash (File.shell_quote path ^ " " ^ args)
    52   | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
    53 
    54 fun system_command cmd =
    55   if bash cmd <> 0 then error ("System command failed: " ^ cmd)
    56   else ();
    57 
    58 
    59 (* directory operations *)
    60 
    61 fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
    62 
    63 fun mkdir path =
    64   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
    65 
    66 fun copy_dir src dst =
    67   if File.eq (src, dst) then ()
    68   else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
    69 
    70 
    71 (* unique tmp files *)
    72 
    73 fun create_tmp_path name ext =
    74   let
    75     val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext);
    76     val _ = File.exists path andalso
    77       raise Fail ("Temporary file already exists: " ^ Path.print path);
    78   in path end;
    79 
    80 fun with_tmp_file name ext f =
    81   let val path = create_tmp_path name ext
    82   in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
    83 
    84 fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
    85 
    86 fun with_tmp_dir name f =
    87   let
    88     val path = create_tmp_path name "";
    89     val _ = mkdirs path;
    90   in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
    91 
    92 
    93 (* fifo *)
    94 
    95 fun with_tmp_fifo f =
    96   with_tmp_file "isabelle-fifo-" ""
    97     (fn path =>
    98       (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
    99         (_, 0) => f path
   100       | (out, _) => error (trim_line out)));
   101 
   102 (* FIXME blocks on Cygwin 1.7.x *)
   103 (* See also http://cygwin.com/ml/cygwin/2010-08/msg00459.html *)
   104 fun bash_output_fifo script f =
   105   with_tmp_fifo (fn fifo =>
   106     uninterruptible (fn restore_attributes => fn () =>
   107       (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
   108         {rc = 0, terminate, ...} =>
   109           (restore_attributes f fifo handle exn => (terminate (); reraise exn))
   110       | {out, ...} => error (trim_line out))) ());
   111 
   112 end;
   113