# HG changeset patch
# User wenzelm
# Date 1646430658 -3600
# Node ID e3475e1d509438d4682bf214e0539a7ea97da81f
# Parent  7870cdaa3f1f923d0a203475276d13a47142bcd0
tuned signature: more robust operation;

diff -r 7870cdaa3f1f -r e3475e1d5094 src/Pure/General/file.scala
--- 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 */