# HG changeset patch
# User wenzelm
# Date 1654070820 -7200
# Node ID 64d48fb1b37b42558aba2bedb9d036b1da6bc2e1
# Parent  a5e0f1c66c265a512f109b25b1f8398d8132f4cb
more robust;

diff -r a5e0f1c66c26 -r 64d48fb1b37b src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue May 31 22:10:48 2022 +0200
+++ b/src/Pure/General/file.scala	Wed Jun 01 10:07:00 2022 +0200
@@ -307,11 +307,19 @@
   }
 
   final class Content_Bytes private[File](val path: Path, content: Bytes) extends Content {
-    def write(dir: Path): Unit = Bytes.write(dir + path, content)
+    def write(dir: Path): Unit = {
+      val full_path = dir + path
+      Isabelle_System.make_directory(full_path.expand.dir)
+      Bytes.write(full_path, content)
+    }
   }
 
   final class Content_String private[File](val path: Path, content: String) extends Content {
-    def write(dir: Path): Unit = File.write(dir + path, content)
+    def write(dir: Path): Unit = {
+      val full_path = dir + path
+      Isabelle_System.make_directory(full_path.expand.dir)
+      File.write(full_path, content)
+    }
   }
 
   final class Content_XML private[File](val path: Path, content: XML.Body) {