wenzelm@40743: (*  Title:      Pure/System/isabelle_system.ML
wenzelm@40743:     Author:     Makarius
wenzelm@40743: 
wenzelm@40743: Isabelle system support.
wenzelm@40743: *)
wenzelm@40743: 
wenzelm@40743: signature ISABELLE_SYSTEM =
wenzelm@40743: sig
wenzelm@40743:   val isabelle_tool: string -> string -> int
wenzelm@40743:   val mkdirs: Path.T -> unit
wenzelm@40745:   val mkdir: Path.T -> unit
wenzelm@40743:   val copy_dir: Path.T -> Path.T -> unit
wenzelm@41307:   val with_tmp_file: string -> (Path.T -> 'a) -> 'a
wenzelm@41307:   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
wenzelm@40743: end;
wenzelm@40743: 
wenzelm@40743: structure Isabelle_System: ISABELLE_SYSTEM =
wenzelm@40743: struct
wenzelm@40743: 
wenzelm@40743: (* system commands *)
wenzelm@40743: 
wenzelm@40743: fun isabelle_tool name args =
wenzelm@40743:   (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
wenzelm@40743:       let val path = dir ^ "/" ^ name in
wenzelm@40743:         if can OS.FileSys.modTime path andalso
wenzelm@40743:           not (OS.FileSys.isDir path) andalso
wenzelm@40743:           OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
wenzelm@40743:         then SOME path
wenzelm@40743:         else NONE
wenzelm@40743:       end handle OS.SysErr _ => NONE) of
wenzelm@40743:     SOME path => bash (File.shell_quote path ^ " " ^ args)
wenzelm@40743:   | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
wenzelm@40743: 
wenzelm@40743: fun system_command cmd =
wenzelm@40743:   if bash cmd <> 0 then error ("System command failed: " ^ cmd)
wenzelm@40743:   else ();
wenzelm@40743: 
wenzelm@40743: 
wenzelm@40743: (* directory operations *)
wenzelm@40743: 
wenzelm@40743: fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
wenzelm@40743: 
wenzelm@40785: fun mkdir path =
wenzelm@40785:   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
wenzelm@40743: 
wenzelm@40743: fun copy_dir src dst =
wenzelm@40743:   if File.eq (src, dst) then ()
wenzelm@40743:   else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
wenzelm@40743: 
wenzelm@41307: 
wenzelm@41307: (* unique tmp files *)
wenzelm@41307: 
wenzelm@41307: local
wenzelm@41307: 
wenzelm@41307: fun fresh_path name =
wenzelm@41307:   let
wenzelm@41307:     val path = File.tmp_path (Path.basic (name ^ serial_string ()));
wenzelm@41307:     val _ = File.exists path andalso
wenzelm@41307:       raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
wenzelm@41307:   in path end;
wenzelm@41307: 
wenzelm@41307: fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
wenzelm@41307: 
wenzelm@41307: in
wenzelm@41307: 
wenzelm@41307: fun with_tmp_file name f =
wenzelm@41307:   let val path = fresh_path name
wenzelm@41307:   in Exn.release (Exn.capture f path before try File.rm path) end;
wenzelm@41307: 
wenzelm@41307: fun with_tmp_dir name f =
wenzelm@41307:   let
wenzelm@41307:     val path = fresh_path name;
wenzelm@41307:     val _ = mkdirs path;
wenzelm@41307:   in Exn.release (Exn.capture f path before try rm_tree path) end;
wenzelm@41307: 
wenzelm@40743: end;
wenzelm@40743: 
wenzelm@41307: end;
wenzelm@41307: