clarified signature: flexible base_dir;
authorwenzelm
Thu Mar 22 17:00:48 2018 +0100 (14 months ago)
changeset 67924b2cdd24e83b6
parent 67923 3e072441c96a
child 67925 74dce5658d4c
clarified signature: flexible base_dir;
src/Pure/System/isabelle_system.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Thu Mar 22 16:39:22 2018 +0100
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Mar 22 17:00:48 2018 +0100
     1.3 @@ -173,10 +173,10 @@
     1.4      File.platform_file(path)
     1.5    }
     1.6  
     1.7 -  def tmp_file(name: String, ext: String = ""): JFile =
     1.8 +  def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
     1.9    {
    1.10      val suffix = if (ext == "") "" else "." + ext
    1.11 -    val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
    1.12 +    val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
    1.13      file.deleteOnExit
    1.14      file
    1.15    }
    1.16 @@ -217,9 +217,9 @@
    1.17      }
    1.18    }
    1.19  
    1.20 -  def tmp_dir(name: String): JFile =
    1.21 +  def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
    1.22    {
    1.23 -    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
    1.24 +    val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
    1.25      dir.deleteOnExit
    1.26      dir
    1.27    }