--- a/src/Pure/Admin/component_jedit.scala Sat Aug 30 12:45:27 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala Sat Aug 30 13:07:29 2025 +0200
@@ -175,8 +175,8 @@
name = file.getName
if !File.is_backup(name)
} {
- progress.bash("patch -p2 < " + File.bash_path(File.path(file)),
- cwd = source_dir, echo = progress.verbose).check
+ val patch = File.read(File.path(file))
+ Isabelle_System.apply_patch(source_dir, patch, strip = 2, progress = progress)
}
progress.echo("Augmenting icons ...")
--- a/src/Pure/System/isabelle_system.scala Sat Aug 30 12:45:27 2025 +0200
+++ b/src/Pure/System/isabelle_system.scala Sat Aug 30 13:07:29 2025 +0200
@@ -509,8 +509,20 @@
Library.terminate_lines(lines)
}
- def apply_patch(base_dir: Path, patch: String, strip: Int = 1): Process_Result =
- Isabelle_System.bash("patch -p" + strip, cwd = base_dir, input = patch).check
+ def apply_patch(base_dir: Path, patch: String,
+ strip: Int = 1,
+ progress: Progress = new Progress
+ ): Unit = {
+ with_tmp_file("patch", ext = "rej") { rej =>
+ val result =
+ Isabelle_System.bash("patch -f -p" + strip + " -r " + File.bash_path(rej),
+ cwd = base_dir, input = patch, progress_stdout = progress.echo_if(progress.verbose, _))
+ if (!result.ok) {
+ val lines = if (rej.is_file) Library.trim_split_lines(File.read(rej)) else Nil
+ error("Failed to apply patch" + if_proper(lines, ":\n") + cat_lines(lines))
+ }
+ }
+ }
def git_clone(url: String, target: Path,
checkout: String = "HEAD",