--- a/src/Pure/General/file.scala Tue May 04 20:40:09 2021 +0200
+++ b/src/Pure/General/file.scala Wed May 05 13:27:30 2021 +0200
@@ -279,14 +279,20 @@
/* 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)))
+ 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)
/* append */
def append(file: JFile, text: String): Unit =
- Files.write(file.toPath, UTF8.bytes(text.toString),
+ Files.write(file.toPath, UTF8.bytes(text),
StandardOpenOption.APPEND, StandardOpenOption.CREATE)
def append(path: Path, text: String): Unit = append(path.file, text)