--- 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) {