67 fun check_bash_function ctxt arg = |
67 fun check_bash_function ctxt arg = |
68 Completion.check_entity Markup.bash_functionN |
68 Completion.check_entity Markup.bash_functionN |
69 (bash_functions () |> map (rpair Position.none)) ctxt arg; |
69 (bash_functions () |> map (rpair Position.none)) ctxt arg; |
70 |
70 |
71 |
71 |
72 (* directory operations *) |
72 (* directory and file operations *) |
|
73 |
|
74 fun scala_function name args = |
|
75 ignore (Scala.function name (space_implode "\000" (map (Path.implode o File.absolute_path) args))); |
73 |
76 |
74 fun system_command cmd = |
77 fun system_command cmd = |
75 if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); |
78 if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); |
76 |
79 |
77 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); |
80 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); |
78 |
81 |
79 fun make_directory path = |
82 fun make_directory path = (scala_function "make_directory" [path]; path); |
80 (Scala.function "make_directory" (Path.implode (File.absolute_path path)); path); |
|
81 |
83 |
82 fun copy_dir src dst = |
84 fun copy_dir src dst = scala_function "copy_dir" [src, dst]; |
83 if File.eq (src, dst) then () |
|
84 else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ()); |
|
85 |
85 |
86 fun copy_file src0 dst0 = |
86 fun copy_file src dst = scala_function "copy_file" [src, dst]; |
87 let |
|
88 val src = Path.expand src0; |
|
89 val dst = Path.expand dst0; |
|
90 val target = if File.is_dir dst then dst + Path.base src else dst; |
|
91 in |
|
92 if File.eq (src, target) then () |
|
93 else |
|
94 ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target)) |
|
95 end; |
|
96 |
87 |
97 fun copy_file_base (base_dir, src0) target_dir = |
88 fun copy_file_base (base_dir, src) target_dir = |
98 let |
89 scala_function "copy_file_base" [base_dir, src, target_dir]; |
99 val src = Path.expand src0; |
|
100 val src_dir = Path.dir src; |
|
101 val _ = |
|
102 if Path.starts_basic src then () |
|
103 else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); |
|
104 in copy_file (base_dir + src) (make_directory (target_dir + src_dir)) end; |
|
105 |
90 |
106 |
91 |
107 (* tmp files *) |
92 (* tmp files *) |
108 |
93 |
109 fun create_tmp_path name ext = |
94 fun create_tmp_path name ext = |