# HG changeset patch
# User wenzelm
# Date 1614607080 -3600
# Node ID 0fb889c361e6c13af22eb3e4e1377dd7d6c4523a
# Parent  2aef2de6b17cb8f71f8e9bebfdb7bb6854b7a658
tuned signature;

diff -r 2aef2de6b17c -r 0fb889c361e6 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Mar 01 08:16:22 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Mar 01 14:58:00 2021 +0100
@@ -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);
 
@@ -111,7 +112,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;