more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
authorwenzelm
Sat Apr 05 22:37:17 2014 +0200 (2014-04-05)
changeset 564281acf2d76ac23
parent 56427 5cbaf18d0dfb
child 56429 bc61161a5bd0
more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
src/Pure/General/file.scala
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/active.scala
     1.1 --- a/src/Pure/General/file.scala	Sat Apr 05 20:08:00 2014 +0200
     1.2 +++ b/src/Pure/General/file.scala	Sat Apr 05 22:37:17 2014 +0200
     1.3 @@ -142,21 +142,5 @@
     1.4    }
     1.5  
     1.6    def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
     1.7 -
     1.8 -
     1.9 -  /* tmp files */
    1.10 -
    1.11 -  def tmp_file(prefix: String): JFile =
    1.12 -  {
    1.13 -    val file = JFile.createTempFile(prefix, null)
    1.14 -    file.deleteOnExit
    1.15 -    file
    1.16 -  }
    1.17 -
    1.18 -  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
    1.19 -  {
    1.20 -    val file = tmp_file(prefix)
    1.21 -    try { body(file) } finally { file.delete }
    1.22 -  }
    1.23  }
    1.24  
     2.1 --- a/src/Pure/System/isabelle_system.scala	Sat Apr 05 20:08:00 2014 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Apr 05 22:37:17 2014 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  import java.util.regex.Pattern
     2.5  import java.io.{File => JFile, BufferedReader, InputStreamReader,
     2.6    BufferedWriter, OutputStreamWriter}
     2.7 +import java.nio.file.Files
     2.8  
     2.9  import scala.util.matching.Regex
    2.10  
    2.11 @@ -91,7 +92,10 @@
    2.12            }
    2.13  
    2.14        val settings =
    2.15 -        File.with_tmp_file("settings") { dump =>
    2.16 +      {
    2.17 +        val dump = JFile.createTempFile("settings", null)
    2.18 +        dump.deleteOnExit
    2.19 +        try {
    2.20            val shell_prefix =
    2.21              if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
    2.22              else Nil
    2.23 @@ -108,6 +112,8 @@
    2.24              }).toMap
    2.25            entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
    2.26          }
    2.27 +        finally { dump.delete }
    2.28 +      }
    2.29        _settings = Some(settings)
    2.30        set_cygwin_root()
    2.31      }
    2.32 @@ -202,6 +208,9 @@
    2.33      else "file:///" + s.replace('\\', '/')
    2.34    }
    2.35  
    2.36 +  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
    2.37 +  def shell_path(file: JFile): String = "'" + posix_path(file) + "'"
    2.38 +
    2.39  
    2.40    /* source files of Isabelle/ML bootstrap */
    2.41  
    2.42 @@ -351,6 +360,30 @@
    2.43    }
    2.44  
    2.45  
    2.46 +  /* tmp files */
    2.47 +
    2.48 +  private def isabelle_tmp_prefix(): JFile =
    2.49 +  {
    2.50 +    val path = Path.explode("$ISABELLE_TMP_PREFIX")
    2.51 +    mkdirs(path)
    2.52 +    platform_file(path)
    2.53 +  }
    2.54 +
    2.55 +  def tmp_file[A](name: String, ext: String = ""): JFile =
    2.56 +  {
    2.57 +    val suffix = if (ext == "") "" else "." + ext
    2.58 +    val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
    2.59 +    file.deleteOnExit
    2.60 +    file
    2.61 +  }
    2.62 +
    2.63 +  def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A =
    2.64 +  {
    2.65 +    val file = tmp_file(name, ext)
    2.66 +    try { body(file) } finally { file.delete }
    2.67 +  }
    2.68 +
    2.69 +
    2.70    /* bash */
    2.71  
    2.72    final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
    2.73 @@ -366,7 +399,7 @@
    2.74      progress_stderr: String => Unit = (_: String) => (),
    2.75      progress_limit: Option[Long] = None): Bash_Result =
    2.76    {
    2.77 -    File.with_tmp_file("isabelle_script") { script_file =>
    2.78 +    with_tmp_file("isabelle_script") { script_file =>
    2.79        File.write(script_file, script)
    2.80        val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
    2.81        proc.stdin.close
    2.82 @@ -401,6 +434,35 @@
    2.83    def bash(script: String): Bash_Result = bash_env(null, null, script)
    2.84  
    2.85  
    2.86 +  /* tmp dirs */
    2.87 +
    2.88 +  private def system_command(cmd: String)
    2.89 +  {
    2.90 +    val res = bash(cmd)
    2.91 +    if (res.rc != 0)
    2.92 +      error(cat_lines(("System command failed: " + cmd) :: res.out_lines ::: res.err_lines))
    2.93 +  }
    2.94 +
    2.95 +  def rm_tree(dir: JFile)
    2.96 +  {
    2.97 +    dir.delete
    2.98 +    if (dir.isDirectory) system_command("rm -r -f " + shell_path(dir))
    2.99 +  }
   2.100 +
   2.101 +  def tmp_dir(name: String): JFile =
   2.102 +  {
   2.103 +    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
   2.104 +    dir.deleteOnExit
   2.105 +    dir
   2.106 +  }
   2.107 +
   2.108 +  def with_tmp_dir[A](name: String)(body: JFile => A): A =
   2.109 +  {
   2.110 +    val dir = tmp_dir(name)
   2.111 +    try { body(dir) } finally { rm_tree(dir) }
   2.112 +  }
   2.113 +
   2.114 +
   2.115    /* system tools */
   2.116  
   2.117    def isabelle_tool(name: String, args: String*): (String, Int) =
     3.1 --- a/src/Pure/Tools/build.scala	Sat Apr 05 20:08:00 2014 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Sat Apr 05 22:37:17 2014 +0200
     3.3 @@ -508,7 +508,7 @@
     3.4  
     3.5      private val parent = info.parent.getOrElse("")
     3.6  
     3.7 -    private val args_file = File.tmp_file("args")
     3.8 +    private val args_file = Isabelle_System.tmp_file("args")
     3.9      File.write(args_file, YXML.string_of_body(
    3.10        if (is_pure(name)) Options.encode(info.options)
    3.11        else
     4.1 --- a/src/Tools/jEdit/src/active.scala	Sat Apr 05 20:08:00 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/active.scala	Sat Apr 05 22:37:17 2014 +0200
     4.3 @@ -32,7 +32,7 @@
     4.4                case XML.Elem(Markup(Markup.BROWSER, _), body) =>
     4.5                  default_thread_pool.submit(() =>
     4.6                    {
     4.7 -                    val graph_file = File.tmp_file("graph")
     4.8 +                    val graph_file = Isabelle_System.tmp_file("graph")
     4.9                      File.write(graph_file, XML.content(body))
    4.10                      Isabelle_System.bash_env(null,
    4.11                        Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),