--- 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 */