# HG changeset patch
# User paulson
# Date 1614610028 0
# Node ID da4334257742d4609cb4c057cd288907a82f4efb
# Parent  d045cdbdf243318a977db8834e9ca2a5aa5d3a0c# Parent  00e0f7724c06b76189ae01c744581ff9218536fe
merged

diff -r 00e0f7724c06 -r da4334257742 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Mar 01 14:46:51 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML	Mon Mar 01 14:47:08 2021 +0000
@@ -71,8 +71,9 @@
 
 (* directory and file operations *)
 
-fun scala_function name args =
-  ignore (Scala.function name (space_implode "\000" (map (Path.implode o File.absolute_path) args)));
+val absolute_path = Path.implode o File.absolute_path;
+fun scala_function0 name = ignore o Scala.function name o space_implode "\000";
+fun scala_function name = scala_function0 name o map absolute_path;
 
 fun make_directory path = (scala_function "make_directory" [path]; path);
 
@@ -81,7 +82,8 @@
 fun copy_file src dst = scala_function "copy_file" [src, dst];
 
 fun copy_file_base (base_dir, src) target_dir =
-  scala_function "copy_file_base" [base_dir, src, target_dir];
+  scala_function0 "copy_file_base"
+    [absolute_path base_dir, Path.implode src, absolute_path target_dir];
 
 
 (* tmp files *)
@@ -111,7 +113,7 @@
 
 fun download url =
   with_tmp_file "download" "" (fn path =>
-   (Scala.function "download" (url ^ "\000" ^ Path.implode (File.absolute_path path));
+   (scala_function0 "download" [url, absolute_path path];
     File.read path));
 
 end;