src/Pure/System/isabelle_system.ML
changeset 73316 8664433956b3
parent 73314 87403fde8cc3
child 73322 5b15eee1a661
equal deleted inserted replaced
73315:d01ca5e9e0da 73316:8664433956b3
    11   val bash: string -> int
    11   val bash: string -> int
    12   val bash_functions: unit -> string list
    12   val bash_functions: unit -> string list
    13   val check_bash_function: Proof.context -> string * Position.T -> string
    13   val check_bash_function: Proof.context -> string * Position.T -> string
    14   val rm_tree: Path.T -> unit
    14   val rm_tree: Path.T -> unit
    15   val make_directory: Path.T -> Path.T
    15   val make_directory: Path.T -> Path.T
    16   val mkdir: Path.T -> unit
       
    17   val copy_dir: Path.T -> Path.T -> unit
    16   val copy_dir: Path.T -> Path.T -> unit
    18   val copy_file: Path.T -> Path.T -> unit
    17   val copy_file: Path.T -> Path.T -> unit
    19   val copy_file_base: Path.T * Path.T -> Path.T -> unit
    18   val copy_file_base: Path.T * Path.T -> Path.T -> unit
    20   val create_tmp_path: string -> string -> Path.T
    19   val create_tmp_path: string -> string -> Path.T
    21   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
    20   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
    78 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
    77 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
    79 
    78 
    80 fun make_directory path =
    79 fun make_directory path =
    81   (Scala.function "make_directory" (Path.implode (File.absolute_path path)); path);
    80   (Scala.function "make_directory" (Path.implode (File.absolute_path path)); path);
    82 
    81 
    83 fun mkdir path =
       
    84   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
       
    85 
       
    86 fun copy_dir src dst =
    82 fun copy_dir src dst =
    87   if File.eq (src, dst) then ()
    83   if File.eq (src, dst) then ()
    88   else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ());
    84   else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ());
    89 
    85 
    90 fun copy_file src0 dst0 =
    86 fun copy_file src0 dst0 =