--- 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")
+ }
}
}
--- 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 */
--- 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
--- 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)))
}
- )
+ }
}
--- 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
--- 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",
--- 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 */
--- 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
- )))
+ ))
+ }
}