diff -r 4fdde010086f -r ee1bd0687c2b src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Mar 03 17:11:43 2022 +0100
+++ b/src/Pure/General/file.scala	Thu Mar 03 17:13:24 2022 +0100
@@ -243,11 +243,13 @@
     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(path: Path)(f: String => String): Unit = change(path.file)(f)
-  def change_lines(path: Path)(f: List[String] => List[String]): Unit = change_lines(path.file)(f)
+  def change_lines(path: Path)(f: List[String] => List[String]): Unit =
+    change_lines(path.file)(f)
 
 
   /* append */