# HG changeset patch # User wenzelm # Date 1601930986 -7200 # Node ID 075f3cbc7546d37e90393e2355f44aebe1bc586b # Parent c7741f767e3e1e91d45cf2bd0859ce58323d467f clarified signature; diff -r c7741f767e3e -r 075f3cbc7546 src/Pure/Admin/build_e.scala --- 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\"`")) } diff -r c7741f767e3e -r 075f3cbc7546 src/Pure/Admin/build_polyml.scala --- 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))) + } + ) } diff -r c7741f767e3e -r 075f3cbc7546 src/Pure/Admin/build_release.scala --- 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 diff -r c7741f767e3e -r 075f3cbc7546 src/Pure/General/file.scala --- 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 =