--- a/src/Pure/General/file.scala Thu Mar 03 17:21:57 2022 +0100
+++ b/src/Pure/General/file.scala Thu Mar 03 17:30:43 2022 +0100
@@ -234,24 +234,6 @@
}
- /* change */
-
- 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)
-
- def change_lines(file: JFile)(f: List[String] => List[String]): Unit =
- change(file)(text => cat_lines(f(split_lines(text))))
-
- def change_lines(path: Path)(f: List[String] => List[String]): Unit =
- change_lines(path.file)(f)
-
-
/* append */
def append(file: JFile, text: String): Unit =
@@ -261,6 +243,20 @@
def append(path: Path, text: String): Unit = append(path.file, text)
+ /* change */
+
+ def change(path: Path, init: Boolean = false)(f: String => String): Unit =
+ {
+ if (init) append(path, "")
+ val x = read(path)
+ val y = f(x)
+ if (x != y) write(path, y)
+ }
+
+ def change_lines(path: Path, init: Boolean = false)(f: List[String] => List[String]): Unit =
+ change(path, init = init)(text => cat_lines(f(split_lines(text))))
+
+
/* eq */
def eq(file1: JFile, file2: JFile): Boolean =