more explicit messages, notably errors;
authorwenzelm
Sat, 30 Aug 2025 13:07:29 +0200
changeset 83080 096f5e72794b
parent 83079 bb2a19ed5305
child 83081 eb0ea0ba8894
more explicit messages, notably errors;
src/Pure/Admin/component_jedit.scala
src/Pure/System/isabelle_system.scala
--- 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",