# HG changeset patch
# User wenzelm
# Date 1646323903 -3600
# Node ID 4fdde010086f4b69b209bd7e7cb64e69cd176d76
# Parent  8f6b8a46f54ca308ca2db1777bcbaff9d3d045f1
clarified signature;

diff -r 8f6b8a46f54c -r 4fdde010086f src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -30,8 +30,9 @@
     {
       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(path) { s =>
+        split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n")
+      }
     }
   }
 
diff -r 8f6b8a46f54c -r 4fdde010086f src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -425,32 +425,32 @@
 
     Mode.list.foreach(_.write(modes_dir))
 
-    File.change_lines(modes_dir + Path.basic("catalog"),
-      _.flatMap(line =>
-          if (line.containsSlice("FILE=\"ml.xml\"") ||
-            line.containsSlice("FILE_NAME_GLOB=\"*.{sml,ml}\"") ||
-            line.containsSlice("FILE_NAME_GLOB=\"*.ftl\"")) Nil
-          else if (line.containsSlice("NAME=\"jamon\"")) {
-            List(
-              """<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>""",
-              "",
-              """<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>""",
-              "",
-              """<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>""",
-              "",
-              """<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>""",
-              "",
-              """<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>""",
-              "",
-              line)
-          }
-          else if (line.containsSlice("NAME=\"sqr\"")) {
-            List(
-              """<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>""",
-              "",
-              line)
-          }
-          else List(line)))
+    File.change_lines(modes_dir + Path.basic("catalog")) { _.flatMap(line =>
+      if (line.containsSlice("FILE=\"ml.xml\"") ||
+        line.containsSlice("FILE_NAME_GLOB=\"*.{sml,ml}\"") ||
+        line.containsSlice("FILE_NAME_GLOB=\"*.ftl\"")) Nil
+      else if (line.containsSlice("NAME=\"jamon\"")) {
+        List(
+          """<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>""",
+          "",
+          """<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>""",
+          "",
+          """<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>""",
+          "",
+          """<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>""",
+          "",
+          """<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>""",
+          "",
+          line)
+      }
+      else if (line.containsSlice("NAME=\"sqr\"")) {
+        List(
+          """<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>""",
+          "",
+          line)
+      }
+      else List(line))
+    }
 
 
     /* doc */
diff -r 8f6b8a46f54c -r 4fdde010086f src/Pure/Admin/build_minisat.scala
--- a/src/Pure/Admin/build_minisat.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Pure/Admin/build_minisat.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -77,8 +77,9 @@
       Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
 
       if (Platform.is_macos) {
-        File.change(build_dir + Path.explode("Makefile"),
-          _.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", ""))
+        File.change(build_dir + Path.explode("Makefile")) {
+          _.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
+        }
       }
       progress.bash("make r", build_dir.file, echo = verbose).check
 
diff -r 8f6b8a46f54c -r 4fdde010086f src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -128,8 +128,8 @@
     /* polyc: directory prefix */
 
     val Header = "#! */bin/sh".r
-    File.change(platform_dir + Path.explode("polyc"), txt =>
-      split_lines(txt) match {
+    File.change(platform_dir + Path.explode("polyc")) { text =>
+      split_lines(text) match {
         case Header() :: lines =>
           val lines1 =
             lines.map(line =>
@@ -137,11 +137,11 @@
               else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
               else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
               else line)
-          cat_lines("#!/usr/bin/env bash" ::lines1)
+          cat_lines("#!/usr/bin/env bash" :: lines1)
         case lines =>
           error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
       }
-    )
+    }
   }
 
 
diff -r 8f6b8a46f54c -r 4fdde010086f src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Pure/Admin/build_release.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -612,16 +612,18 @@
 
         platform match {
           case Platform.Family.linux_arm | Platform.Family.linux =>
-            File.change(isabelle_target + jedit_options,
-              _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
+            File.change(isabelle_target + jedit_options) {
+              _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")
+            }
 
-            File.change(isabelle_target + jedit_props,
+            File.change(isabelle_target + jedit_props) {
               _.replaceAll("console.fontsize=.*", "console.fontsize=18")
                .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
                .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
                .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
                .replaceAll("view.fontsize=.*", "view.fontsize=24")
-               .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
+               .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")
+            }
 
             make_isabelle_options(
               isabelle_target + Path.explode("Isabelle.options"), java_options)
@@ -635,9 +637,10 @@
 
 
           case Platform.Family.macos =>
-            File.change(isabelle_target + jedit_props,
+            File.change(isabelle_target + jedit_props) {
               _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
-               .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
+               .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
+            }
 
 
             // macOS application bundle
@@ -675,8 +678,9 @@
 
 
           case Platform.Family.windows =>
-            File.change(isabelle_target + jedit_props,
-              _.replaceAll("foldPainter=.*", "foldPainter=Square"))
+            File.change(isabelle_target + jedit_props) {
+              _.replaceAll("foldPainter=.*", "foldPainter=Square")
+            }
 
 
             // application launcher
diff -r 8f6b8a46f54c -r 4fdde010086f src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Pure/Admin/build_spass.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -82,9 +82,10 @@
       val build_dir = tmp_dir + Path.basic(archive_base_name)
 
       if (Platform.is_windows) {
-        File.change(build_dir + Path.basic("misc.c"),
+        File.change(build_dir + Path.basic("misc.c")) {
           _.replace("""#include "execinfo.h" """, "")
-           .replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }"))
+           .replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")
+        }
       }
 
       Isabelle_System.bash("make",
diff -r 8f6b8a46f54c -r 4fdde010086f src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Pure/General/file.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -236,18 +236,18 @@
 
   /* change */
 
-  def change(file: JFile, f: String => String): Unit =
+  def change(file: JFile)(f: String => String): Unit =
   {
     val x = read(file)
     val y = f(x)
     if (x != y) write(file, y)
   }
 
-  def change_lines(file: JFile, f: List[String] => List[String]): Unit =
-    change(file, text => cat_lines(f(split_lines(text))))
+  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(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)
 
 
   /* append */
diff -r 8f6b8a46f54c -r 4fdde010086f src/Tools/VSCode/src/vscode_setup.scala
--- a/src/Tools/VSCode/src/vscode_setup.scala	Thu Mar 03 16:46:05 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Thu Mar 03 17:11:43 2022 +0100
@@ -60,13 +60,14 @@
     val checksum2 = file_checksum(workbench_css)
 
     val file_name = workbench_css.file_name
-    File.change(dir + Path.explode("app/product.json"), text =>
+    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
-      )))
+      ))
+    }
   }