src/Pure/System/isabelle_system.scala
changeset 62545 8ebffdaf2ce2
parent 62543 57f379ef662f
child 62573 27f90319a499
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 07 15:21:50 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 07 18:20:22 2016 +0100
@@ -167,7 +167,7 @@
 
   def mkdirs(path: Path): Unit =
     if (!path.is_dir) {
-      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
+      bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"")
       if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
     }
 
@@ -308,11 +308,7 @@
     progress_limit: Option[Long] = None,
     strict: Boolean = true): Process_Result =
   {
-    with_tmp_file("isabelle_script") { script_file =>
-      File.write(script_file, script)
-      Bash.process(cwd, env, false, File.standard_path(script_file)).
-        result(progress_stdout, progress_stderr, progress_limit, strict)
-    }
+    Bash.process(script, cwd, env).result(progress_stdout, progress_stderr, progress_limit, strict)
   }
 
 
@@ -342,7 +338,7 @@
     bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
 
   def hg(cmd_line: String, cwd: Path = Path.current): Process_Result =
-    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
+    bash("cd " + File.bash_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)