# HG changeset patch
# User wenzelm
# Date 1646324517 -3600
# Node ID c33e75542ffec810f0c67af85a227d46da2b2933
# Parent  b0910e6c13209daea8b2cc3336baf490a2388c52
tuned;

diff -r b0910e6c1320 -r c33e75542ffe src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Thu Mar 03 17:15:30 2022 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Thu Mar 03 17:21:57 2022 +0100
@@ -30,9 +30,7 @@
     {
       def change_line(line: String, p: (String, String)): String =
         line.replaceAll(p._1 + "=.*", Properties.Eq(p))
-      File.change(path) { s =>
-        split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n")
-      }
+      File.change_lines(path) { _.map(line => changed.foldLeft(line)(change_line)) }
     }
   }
 
diff -r b0910e6c1320 -r c33e75542ffe src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Thu Mar 03 17:15:30 2022 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Thu Mar 03 17:21:57 2022 +0100
@@ -128,19 +128,17 @@
     /* polyc: directory prefix */
 
     val Header = "#! */bin/sh".r
-    File.change(platform_dir + Path.explode("polyc")) { text =>
-      split_lines(text) match {
-        case Header() :: lines =>
-          val lines1 =
-            lines.map(line =>
-              if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
-              else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
-              else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
-              else line)
-          cat_lines("#!/usr/bin/env bash" :: lines1)
-        case lines =>
-          error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
-      }
+    File.change_lines(platform_dir + Path.explode("polyc")) {
+      case Header() :: lines =>
+        val lines1 =
+          lines.map(line =>
+            if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
+            else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
+            else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
+            else line)
+        "#!/usr/bin/env bash" :: lines1
+      case lines =>
+        error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
     }
   }
 
diff -r b0910e6c1320 -r c33e75542ffe src/Tools/VSCode/src/vscode_setup.scala
--- a/src/Tools/VSCode/src/vscode_setup.scala	Thu Mar 03 17:15:30 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Thu Mar 03 17:21:57 2022 +0100
@@ -60,13 +60,11 @@
     val checksum2 = file_checksum(workbench_css)
 
     val file_name = workbench_css.file_name
-    File.change(dir + Path.explode("app/product.json")) { text =>
-      cat_lines(split_lines(text).map(line =>
-        if (line.containsSlice(file_name) && line.contains(checksum1)) {
-          line.replace(checksum1, checksum2)
-        }
-        else line
-      ))
+    File.change_lines(dir + Path.explode("app/product.json")) { _.map(line =>
+      if (line.containsSlice(file_name) && line.contains(checksum1)) {
+        line.replace(checksum1, checksum2)
+      }
+      else line)
     }
   }