diff -r c7741f767e3e -r 075f3cbc7546 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Oct 05 22:23:17 2020 +0200
+++ b/src/Pure/General/file.scala	Mon Oct 05 22:49:46 2020 +0200
@@ -269,6 +269,12 @@
   }
 
 
+  /* change */
+
+  def change(file: JFile, f: String => String): Unit = write(file, f(read(file)))
+  def change(path: Path, f: String => String): Unit = write(path, f(read(path)))
+
+
   /* append */
 
   def append(file: JFile, text: CharSequence): Unit =