--- a/src/Pure/Admin/build_e.scala Mon Oct 05 22:23:17 2020 +0200
+++ b/src/Pure/Admin/build_e.scala Mon Oct 05 22:49:46 2020 +0200
@@ -47,11 +47,10 @@
val runepar_path = platform_dir + Path.basic("runepar.pl")
Isabelle_System.download(runepar_url, runepar_path, progress = progress)
- File.write(runepar_path,
- File.read(runepar_path)
- .replace("#!/usr/bin/perl", "#!/usr/bin/env perl")
- .replace("bin/eprover", "$ENV{E_HOME}/eprover")
- .replace("bin/eproof", "$ENV{E_HOME}/eproof"))
+ File.change(runepar_path,
+ _.replace("#!/usr/bin/perl", "#!/usr/bin/env perl")
+ .replace("bin/eprover", "$ENV{E_HOME}/eprover")
+ .replace("bin/eproof", "$ENV{E_HOME}/eproof"))
File.set_executable(runepar_path, true)
@@ -98,9 +97,7 @@
val eproof_ram = platform_dir + Path.basic("eproof_ram")
if (eproof_ram.is_file) {
- File.write(eproof_ram,
- File.read(eproof_ram)
- .replace("EXECPATH=.", "EXECPATH=`dirname \"$0\"`"))
+ File.change(eproof_ram, _.replace("EXECPATH=.", "EXECPATH=`dirname \"$0\"`"))
}
--- a/src/Pure/Admin/build_polyml.scala Mon Oct 05 22:23:17 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala Mon Oct 05 22:49:46 2020 +0200
@@ -171,25 +171,21 @@
/* polyc: directory prefix */
- {
- val polyc_path = target + Path.explode("polyc")
-
- val Header = "#! */bin/sh".r
- val polyc_patched =
- split_lines(File.read(polyc_path)) 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.write(polyc_path, polyc_patched)
- }
+ val Header = "#! */bin/sh".r
+ File.change(target + Path.explode("polyc"), txt =>
+ split_lines(txt) 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)))
+ }
+ )
}
--- a/src/Pure/Admin/build_release.scala Mon Oct 05 22:23:17 2020 +0200
+++ b/src/Pure/Admin/build_release.scala Mon Oct 05 22:49:46 2020 +0200
@@ -50,13 +50,7 @@
/* patch release */
- private def change_file(dir: Path, name: String, f: String => String)
- {
- val file = dir + Path.explode(name)
- File.write(file, f(File.read(file)))
- }
-
- private val getsettings_file: String = "lib/scripts/getsettings"
+ private val getsettings_path = Path.explode("lib/scripts/getsettings")
private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
@@ -66,20 +60,19 @@
for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
{
- change_file(dir, name,
+ File.change(dir + Path.explode(name),
s =>
s.replaceAllLiterally("val is_identified = false", "val is_identified = true")
.replaceAllLiterally("val is_official = false", "val is_official = " + is_official))
}
- change_file(dir, getsettings_file,
- s =>
- s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
- .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
- "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
+ File.change(dir + getsettings_path,
+ _.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
+ .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
+ "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
- change_file(dir, "lib/html/library_index_header.template",
- s => s.replaceAllLiterally("{ISABELLE}", release.dist_name))
+ File.change(dir + Path.explode("lib/html/library_index_header.template"),
+ _.replaceAllLiterally("{ISABELLE}", release.dist_name))
for {
name <-
@@ -88,11 +81,11 @@
"src/Pure/System/distribution.scala",
"lib/Tools/version") }
{
- change_file(dir, name,
+ File.change(dir + Path.explode(name),
s => s.replaceAllLiterally("repository version", release.dist_version))
}
- change_file(dir, "README",
+ File.change(dir + Path.explode("README"),
s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version))
}
@@ -307,7 +300,7 @@
val archive_ident =
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
- val getsettings = Path.explode(release.dist_name + "/" + getsettings_file)
+ val getsettings = Path.explode(release.dist_name) + getsettings_path
execute_tar(tmp_dir, "-xzf " +
File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
split_lines(File.read(tmp_dir + getsettings))
@@ -505,18 +498,16 @@
platform match {
case Platform.Family.linux =>
- File.write(isabelle_target + jedit_options,
- File.read(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.write(isabelle_target + jedit_props,
- File.read(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"))
+ 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"))
File.write(isabelle_target + Path.explode("Isabelle.options"),
terminate_lines(java_options_title :: java_options))
@@ -542,11 +533,10 @@
case Platform.Family.macos =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
- .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
- .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
+ File.change(isabelle_target + jedit_props,
+ _.replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
+ .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
+ .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// MacOS application bundle
@@ -601,11 +591,10 @@
case Platform.Family.windows =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*",
+ File.change(isabelle_target + jedit_props,
+ _.replaceAll("lookAndFeel=.*",
"lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
- .replaceAll("foldPainter=.*", "foldPainter=Square"))
+ .replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
--- a/src/Pure/General/file.scala Mon Oct 05 22:23:17 2020 +0200
+++ b/src/Pure/General/file.scala Mon Oct 05 22:49:46 2020 +0200
@@ -269,6 +269,12 @@
}
+ /* change */
+
+ def change(file: JFile, f: String => String): Unit = write(file, f(read(file)))
+ def change(path: Path, f: String => String): Unit = write(path, f(read(path)))
+
+
/* append */
def append(file: JFile, text: CharSequence): Unit =