more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);

--- a/src/Pure/General/file.ML	Sat Feb 27 16:33:16 2021 +0100
+++ b/src/Pure/General/file.ML	Sat Feb 27 17:25:54 2021 +0100
@@ -11,6 +11,7 @@
   val bash_path: Path.T -> string
   val bash_paths: Path.T list -> string
   val bash_platform_path: Path.T -> string
+  val absolute_path: Path.T -> Path.T
   val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
@@ -56,15 +57,16 @@
 
 (* full_path *)
 
+val absolute_path =
+  Path.expand #> (fn path =>
+    if Path.is_absolute path then path
+    else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path);
+
 fun full_path dir path =
   let
     val path' = Path.expand path;
     val _ = Path.is_current path' andalso error "Bad file specification";
-    val path'' = dir + path';
-  in
-    if Path.is_absolute path'' then path''
-    else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path''
-  end;
+  in absolute_path (dir + path') end;
 
 
 (* tmp_path *)

--- a/src/Pure/System/isabelle_system.ML	Sat Feb 27 16:33:16 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sat Feb 27 17:25:54 2021 +0100
@@ -78,13 +78,7 @@
 fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
 
 fun make_directory path =
-  let
-    val _ =
-      if File.is_dir path then ()
-      else
-       (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\"");
-        if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
-  in path end;
+  (Scala.function "make_directory" (Path.implode (File.absolute_path path)); path);
 
 fun mkdir path =
   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);

--- a/src/Pure/System/isabelle_system.scala	Sat Feb 27 16:33:16 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Feb 27 17:25:54 2021 +0100
@@ -191,13 +191,17 @@
 
   def make_directory(path: Path): Path =
   {
-    if (!path.is_dir) {
-      bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"")
-      if (!path.is_dir) error("Failed to create directory: " + path.absolute)
-    }
+    try { Files.createDirectories(path.file.toPath) }
+    catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
     path
   }
 
+  object Make_Directory extends Scala.Fun("make_directory")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String = { make_directory(Path.explode(arg)); "" }
+  }
+
   def new_directory(path: Path): Path =
     if (path.is_dir) error("Directory already exists: " + path.absolute)
     else make_directory(path)

--- a/src/Pure/System/scala.scala	Sat Feb 27 16:33:16 2021 +0100
+++ b/src/Pure/System/scala.scala	Sat Feb 27 17:25:54 2021 +0100
@@ -245,4 +245,5 @@
   Doc.Doc_Names,
   Bash.Process,
   Bibtex.Check_Database,
+  Isabelle_System.Make_Directory,
   Isabelle_Tool.Isabelle_Tools)