--- a/src/Pure/General/file.scala Fri Mar 04 21:47:57 2022 +0100
+++ b/src/Pure/General/file.scala Fri Mar 04 22:50:58 2022 +0100
@@ -245,16 +245,18 @@
/* change */
- def change(path: Path, init: Boolean = false)(f: String => String): Unit =
+ def change(path: Path, init: Boolean = false, strict: Boolean = false)(f: String => String): Unit =
{
if (!path.is_file && init) write(path, "")
val x = read(path)
val y = f(x)
if (x != y) write(path, y)
+ else if (strict) error("Unchanged file: " + path)
}
- 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))))
+ def change_lines(path: Path, init: Boolean = false, strict: Boolean = false)(
+ f: List[String] => List[String]): Unit =
+ change(path, init = init, strict = strict)(text => cat_lines(f(split_lines(text))))
/* eq */