clarified signature;
authorwenzelm
Sat, 05 Mar 2022 11:12:26 +0100
changeset 75220 1cbdf9cfc94b
parent 75219 6d1b64d76b57
child 75221 ea65e18c5614
clarified signature;
src/Pure/Admin/build_jedit.scala
src/Pure/General/path.scala
src/Pure/System/isabelle_system.scala
--- a/src/Pure/Admin/build_jedit.scala	Sat Mar 05 10:57:58 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala	Sat Mar 05 11:12:26 2022 +0100
@@ -472,10 +472,7 @@
 
     /* diff */
 
-    Isabelle_System.bash(
-      "diff -ru " + Bash.string(jedit) + " " + Bash.string(jedit_patched) +
-        " > " + Bash.string(jedit + ".patch"),
-      cwd = component_dir.file).check_rc(_ <= 1)
+    Isabelle_System.make_patch(component_dir, Path.basic(jedit), Path.basic(jedit_patched))
 
     if (!original) Isabelle_System.rm_tree(jedit_dir)
 
--- a/src/Pure/General/path.scala	Sat Mar 05 10:57:58 2022 +0100
+++ b/src/Pure/General/path.scala	Sat Mar 05 11:12:26 2022 +0100
@@ -233,6 +233,7 @@
   def tar: Path = ext("tar")
   def gz: Path = ext("gz")
   def log: Path = ext("log")
+  def patch: Path = ext("patch")
 
   def backup: Path =
   {
--- a/src/Pure/System/isabelle_system.scala	Sat Mar 05 10:57:58 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Mar 05 11:12:26 2022 +0100
@@ -437,6 +437,15 @@
     else error("Expected to find GNU tar executable")
   }
 
+  def make_patch(base_dir: Path, src: Path, dst: Path, target_dir: Path = Path.current): Path =
+  {
+    val target = target_dir + src.base.patch
+    Isabelle_System.bash(
+      "diff -ru " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(target),
+      cwd = base_dir.file).check_rc(_ <= 1)
+    (base_dir + target).expand
+  }
+
   def hostname(): String = bash("hostname -s").check.out
 
   def open(arg: String): Unit =