clarified signature;
authorwenzelm
Wed, 05 May 2021 13:27:30 +0200
changeset 73883 27659455c592
parent 73882 0732f66ce514
child 73884 ac8feb094bd4
clarified signature;
src/Pure/General/file.scala
--- 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)