# HG changeset patch
# User wenzelm
# Date 1396730237 -7200
# Node ID 1acf2d76ac23014cb76c4fed1de9beaeff8ac363
# Parent  5cbaf18d0dfb0f61223c19572098679fc082198a
more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;

diff -r 5cbaf18d0dfb -r 1acf2d76ac23 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Apr 05 20:08:00 2014 +0200
+++ b/src/Pure/General/file.scala	Sat Apr 05 22:37:17 2014 +0200
@@ -142,21 +142,5 @@
   }
 
   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
-
-
-  /* tmp files */
-
-  def tmp_file(prefix: String): JFile =
-  {
-    val file = JFile.createTempFile(prefix, null)
-    file.deleteOnExit
-    file
-  }
-
-  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
-  {
-    val file = tmp_file(prefix)
-    try { body(file) } finally { file.delete }
-  }
 }
 
diff -r 5cbaf18d0dfb -r 1acf2d76ac23 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Apr 05 20:08:00 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Apr 05 22:37:17 2014 +0200
@@ -11,6 +11,7 @@
 import java.util.regex.Pattern
 import java.io.{File => JFile, BufferedReader, InputStreamReader,
   BufferedWriter, OutputStreamWriter}
+import java.nio.file.Files
 
 import scala.util.matching.Regex
 
@@ -91,7 +92,10 @@
           }
 
       val settings =
-        File.with_tmp_file("settings") { dump =>
+      {
+        val dump = JFile.createTempFile("settings", null)
+        dump.deleteOnExit
+        try {
           val shell_prefix =
             if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
             else Nil
@@ -108,6 +112,8 @@
             }).toMap
           entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
         }
+        finally { dump.delete }
+      }
       _settings = Some(settings)
       set_cygwin_root()
     }
@@ -202,6 +208,9 @@
     else "file:///" + s.replace('\\', '/')
   }
 
+  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
+  def shell_path(file: JFile): String = "'" + posix_path(file) + "'"
+
 
   /* source files of Isabelle/ML bootstrap */
 
@@ -351,6 +360,30 @@
   }
 
 
+  /* tmp files */
+
+  private def isabelle_tmp_prefix(): JFile =
+  {
+    val path = Path.explode("$ISABELLE_TMP_PREFIX")
+    mkdirs(path)
+    platform_file(path)
+  }
+
+  def tmp_file[A](name: String, ext: String = ""): JFile =
+  {
+    val suffix = if (ext == "") "" else "." + ext
+    val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
+    file.deleteOnExit
+    file
+  }
+
+  def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A =
+  {
+    val file = tmp_file(name, ext)
+    try { body(file) } finally { file.delete }
+  }
+
+
   /* bash */
 
   final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
@@ -366,7 +399,7 @@
     progress_stderr: String => Unit = (_: String) => (),
     progress_limit: Option[Long] = None): Bash_Result =
   {
-    File.with_tmp_file("isabelle_script") { script_file =>
+    with_tmp_file("isabelle_script") { script_file =>
       File.write(script_file, script)
       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
       proc.stdin.close
@@ -401,6 +434,35 @@
   def bash(script: String): Bash_Result = bash_env(null, null, script)
 
 
+  /* tmp dirs */
+
+  private def system_command(cmd: String)
+  {
+    val res = bash(cmd)
+    if (res.rc != 0)
+      error(cat_lines(("System command failed: " + cmd) :: res.out_lines ::: res.err_lines))
+  }
+
+  def rm_tree(dir: JFile)
+  {
+    dir.delete
+    if (dir.isDirectory) system_command("rm -r -f " + shell_path(dir))
+  }
+
+  def tmp_dir(name: String): JFile =
+  {
+    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
+    dir.deleteOnExit
+    dir
+  }
+
+  def with_tmp_dir[A](name: String)(body: JFile => A): A =
+  {
+    val dir = tmp_dir(name)
+    try { body(dir) } finally { rm_tree(dir) }
+  }
+
+
   /* system tools */
 
   def isabelle_tool(name: String, args: String*): (String, Int) =
diff -r 5cbaf18d0dfb -r 1acf2d76ac23 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Apr 05 20:08:00 2014 +0200
+++ b/src/Pure/Tools/build.scala	Sat Apr 05 22:37:17 2014 +0200
@@ -508,7 +508,7 @@
 
     private val parent = info.parent.getOrElse("")
 
-    private val args_file = File.tmp_file("args")
+    private val args_file = Isabelle_System.tmp_file("args")
     File.write(args_file, YXML.string_of_body(
       if (is_pure(name)) Options.encode(info.options)
       else
diff -r 5cbaf18d0dfb -r 1acf2d76ac23 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Sat Apr 05 20:08:00 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala	Sat Apr 05 22:37:17 2014 +0200
@@ -32,7 +32,7 @@
               case XML.Elem(Markup(Markup.BROWSER, _), body) =>
                 default_thread_pool.submit(() =>
                   {
-                    val graph_file = File.tmp_file("graph")
+                    val graph_file = Isabelle_System.tmp_file("graph")
                     File.write(graph_file, XML.content(body))
                     Isabelle_System.bash_env(null,
                       Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),