src/Pure/System/isabelle_system.scala
changeset 56477 57b5c8db55f1
parent 56449 f0592485b7fb
child 56599 c4424d8c890f
     1.1 --- a/src/Pure/System/isabelle_system.scala	Tue Apr 08 22:24:00 2014 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Apr 08 23:05:21 2014 +0200
     1.3 @@ -10,8 +10,9 @@
     1.4  
     1.5  import java.util.regex.Pattern
     1.6  import java.io.{File => JFile, BufferedReader, InputStreamReader,
     1.7 -  BufferedWriter, OutputStreamWriter}
     1.8 -import java.nio.file.Files
     1.9 +  BufferedWriter, OutputStreamWriter, IOException}
    1.10 +import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
    1.11 +import java.nio.file.attribute.BasicFileAttributes
    1.12  import java.net.{URL, URLDecoder, MalformedURLException}
    1.13  
    1.14  import scala.util.matching.Regex
    1.15 @@ -104,7 +105,7 @@
    1.16              shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    1.17            val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
    1.18            if (rc != 0) error(output)
    1.19 -  
    1.20 +
    1.21            val entries =
    1.22              (for (entry <- File.read(dump) split "\0" if entry != "") yield {
    1.23                val i = entry.indexOf('=')
    1.24 @@ -394,6 +395,47 @@
    1.25    }
    1.26  
    1.27  
    1.28 +  /* tmp dirs */
    1.29 +
    1.30 +  def rm_tree(root: JFile)
    1.31 +  {
    1.32 +    root.delete
    1.33 +    if (root.isDirectory) {
    1.34 +      Files.walkFileTree(root.toPath,
    1.35 +        new SimpleFileVisitor[JPath] {
    1.36 +          override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
    1.37 +          {
    1.38 +            Files.delete(file)
    1.39 +            FileVisitResult.CONTINUE
    1.40 +          }
    1.41 +
    1.42 +          override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
    1.43 +          {
    1.44 +            if (e == null) {
    1.45 +              Files.delete(dir)
    1.46 +              FileVisitResult.CONTINUE
    1.47 +            }
    1.48 +            else throw e
    1.49 +          }
    1.50 +        }
    1.51 +      )
    1.52 +    }
    1.53 +  }
    1.54 +
    1.55 +  def tmp_dir(name: String): JFile =
    1.56 +  {
    1.57 +    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
    1.58 +    dir.deleteOnExit
    1.59 +    dir
    1.60 +  }
    1.61 +
    1.62 +  def with_tmp_dir[A](name: String)(body: JFile => A): A =
    1.63 +  {
    1.64 +    val dir = tmp_dir(name)
    1.65 +    try { body(dir) } finally { rm_tree(dir) }
    1.66 +  }
    1.67 +
    1.68 +
    1.69    /* bash */
    1.70  
    1.71    final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
    1.72 @@ -444,35 +486,6 @@
    1.73    def bash(script: String): Bash_Result = bash_env(null, null, script)
    1.74  
    1.75  
    1.76 -  /* tmp dirs */
    1.77 -
    1.78 -  private def system_command(cmd: String)
    1.79 -  {
    1.80 -    val res = bash(cmd)
    1.81 -    if (res.rc != 0)
    1.82 -      error(cat_lines(("System command failed: " + cmd) :: res.out_lines ::: res.err_lines))
    1.83 -  }
    1.84 -
    1.85 -  def rm_tree(dir: JFile)
    1.86 -  {
    1.87 -    dir.delete
    1.88 -    if (dir.isDirectory) system_command("rm -r -f " + shell_path(dir))
    1.89 -  }
    1.90 -
    1.91 -  def tmp_dir(name: String): JFile =
    1.92 -  {
    1.93 -    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
    1.94 -    dir.deleteOnExit
    1.95 -    dir
    1.96 -  }
    1.97 -
    1.98 -  def with_tmp_dir[A](name: String)(body: JFile => A): A =
    1.99 -  {
   1.100 -    val dir = tmp_dir(name)
   1.101 -    try { body(dir) } finally { rm_tree(dir) }
   1.102 -  }
   1.103 -
   1.104 -
   1.105    /* system tools */
   1.106  
   1.107    def isabelle_tool(name: String, args: String*): (String, Int) =