diff -r c33e75542ffe -r 481ad7da73a9 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Mar 03 17:21:57 2022 +0100
+++ b/src/Pure/General/file.scala	Thu Mar 03 17:30:43 2022 +0100
@@ -234,24 +234,6 @@
   }
 
 
-  /* change */
-
-  def change(file: JFile)(f: String => String): Unit =
-  {
-    val x = read(file)
-    val y = f(x)
-    if (x != y) write(file, y)
-  }
-
-  def change(path: Path)(f: String => String): Unit = change(path.file)(f)
-
-  def change_lines(file: JFile)(f: List[String] => List[String]): Unit =
-    change(file)(text => cat_lines(f(split_lines(text))))
-
-  def change_lines(path: Path)(f: List[String] => List[String]): Unit =
-    change_lines(path.file)(f)
-
-
   /* append */
 
   def append(file: JFile, text: String): Unit =
@@ -261,6 +243,20 @@
   def append(path: Path, text: String): Unit = append(path.file, text)
 
 
+  /* change */
+
+  def change(path: Path, init: Boolean = false)(f: String => String): Unit =
+  {
+    if (init) append(path, "")
+    val x = read(path)
+    val y = f(x)
+    if (x != y) write(path, y)
+  }
+
+  def change_lines(path: Path, init: Boolean = false)(f: List[String] => List[String]): Unit =
+    change(path, init = init)(text => cat_lines(f(split_lines(text))))
+
+
   /* eq */
 
   def eq(file1: JFile, file2: JFile): Boolean =