more robust: avoid race condition wrt. cleanup of ML process, e.g. relevant for "$ISABELLE_TMP/rat.ML" in theory Codegen.Further;
--- a/src/Pure/System/isabelle_system.scala Thu Sep 13 16:15:05 2018 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Sep 13 16:30:07 2018 +0200
@@ -197,14 +197,16 @@
new SimpleFileVisitor[JPath] {
override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
{
- Files.deleteIfExists(file)
+ try { Files.deleteIfExists(file) }
+ catch { case _: IOException => }
FileVisitResult.CONTINUE
}
override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
{
if (e == null) {
- Files.deleteIfExists(dir)
+ try { Files.deleteIfExists(dir) }
+ catch { case _: IOException => }
FileVisitResult.CONTINUE
}
else throw e