clarified signature: closer to regular bash();
authorwenzelm
Fri, 12 Sep 2025 17:07:21 +0200
changeset 83138 c66d77fb729e
parent 83136 b6e117b5d0f0
child 83139 c87375585b9f
clarified signature: closer to regular bash();
src/Pure/Admin/component_polyml.scala
src/Pure/System/isabelle_platform.scala
src/Pure/System/nodejs.scala
src/Tools/VSCode/src/component_vscodium.scala
--- a/src/Pure/Admin/component_polyml.scala	Thu Sep 11 10:47:25 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Fri Sep 12 17:07:21 2025 +0200
@@ -70,15 +70,17 @@
     val target_dir = root + Path.explode("target")
 
     progress.echo("Building GMP library ...")
-    platform_context.execute(root,
-      "[ -f Makefile ] && make distclean",
-      "./configure --disable-static --enable-shared --enable-cxx" +
-        " --build=" + platform_arch + "-" + platform_os +
-        """ --prefix="$PWD/target" """ + Bash.strings(options),
-      "rm -rf target",
-      "make",
-      "make check",
-      "make install")
+    platform_context.bash(
+      Library.make_lines(
+        "set -e",
+        "[ -f Makefile ] && make distclean",
+        "./configure --disable-static --enable-shared --enable-cxx" +
+          " --build=" + platform_arch + "-" + platform_os +
+          """ --prefix="$PWD/target" """ + Bash.strings(options),
+        "rm -rf target",
+        "make",
+        "make check",
+        "make install"), cwd = root).check
 
     if (platform.is_windows) {
       val bin_dir = target_dir + Path.explode("bin")
@@ -143,14 +145,16 @@
         case None => ""
       }
 
-    platform_context.execute(root,
-      platform_info.setup,
-      gmp_setup,
-      "[ -f Makefile ] && make distclean",
-      """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
-      "rm -rf target",
-      "make",
-      "make install")
+    platform_context.bash(
+      Library.make_lines(
+        "set -e",
+        platform_info.setup,
+        gmp_setup,
+        "[ -f Makefile ] && make distclean",
+        """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
+        "rm -rf target",
+        "make",
+        "make install"), cwd = root).check
 
 
     /* sha1 library */
@@ -160,7 +164,7 @@
         case Some(dir) =>
           val platform_path = Path.explode(platform.ISABELLE_PLATFORM(windows = true, apple = true))
           val platform_dir = dir + platform_path
-          platform_context.execute(dir, "./build " + File.bash_path(platform_path))
+          platform_context.bash("./build " + File.bash_path(platform_path), cwd = dir).check
           File.read_dir(platform_dir).map(entry => platform_dir + Path.basic(entry))
         case None => Nil
       }
--- a/src/Pure/System/isabelle_platform.scala	Thu Sep 11 10:47:25 2025 +0200
+++ b/src/Pure/System/isabelle_platform.scala	Fri Sep 12 17:07:21 2025 +0200
@@ -68,13 +68,11 @@
     def standard_path(path: Path): String =
       mingw.standard_path(File.platform_path(path))
 
-    def execute(cwd: Path, script_lines: String*): Process_Result = {
-      val script = cat_lines("set -e" :: script_lines.toList)
-      val script1 =
+    def bash(script: String, cwd: Path = Path.current): Process_Result =
+      progress.bash(
         if (is_macos_arm) "arch -arch arm64 bash -c " + Bash.string(script)
-        else mingw.bash_script(script)
-      progress.bash(script1, cwd = cwd, echo = progress.verbose).check
-    }
+        else mingw.bash_script(script),
+        cwd = cwd, echo = progress.verbose)
   }
 }
 
--- a/src/Pure/System/nodejs.scala	Thu Sep 11 10:47:25 2025 +0200
+++ b/src/Pure/System/nodejs.scala	Fri Sep 12 17:07:21 2025 +0200
@@ -68,11 +68,12 @@
 
     def install(name: String, production: Boolean = false): Unit = {
       progress.echo("Installing " + name + " ...")
-      platform_context.execute(path,
+      platform_context.bash(
         Library.make_lines(
+          "set -e",
           path_setup,
           "npm install --global " + if_proper(production, "--production ") + Bash.string(name)
-        )).check
+        ), cwd = path).check
     }
   }
 
--- a/src/Tools/VSCode/src/component_vscodium.scala	Thu Sep 11 10:47:25 2025 +0200
+++ b/src/Tools/VSCode/src/component_vscodium.scala	Fri Sep 12 17:07:21 2025 +0200
@@ -195,7 +195,8 @@
       Isabelle_System.git_clone(vscodium_repository, build_dir, checkout = vscodium_version)
 
       progress.echo("Getting VSCode repository ...")
-      platform_context.execute(build_dir, environment(build_dir) + "\n" + "./get_repo.sh").check
+      platform_context.bash(
+        environment(build_dir) + "\n" + "./get_repo.sh", cwd = build_dir).check
     }
 
     def platform_name: String = platform_context.ISABELLE_PLATFORM
@@ -316,13 +317,15 @@
 
       progress.echo("Preparing VSCode ...")
       Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) {
-        platform_context.execute(build_dir,
-          "set -e",
-          build_context.environment(build_dir),
-          node_dir.path_setup,
-          "./prepare_vscode.sh",
-          // enforce binary diff of code.xpm
-          "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm").check
+        platform_context.bash(
+          Library.make_lines(
+            "set -e",
+            build_context.environment(build_dir),
+            node_dir.path_setup,
+            "./prepare_vscode.sh",
+            // enforce binary diff of code.xpm
+            "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"),
+          cwd = build_dir).check
         Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
           diff_options = "--exclude=.git --exclude=node_modules")
       }
@@ -391,16 +394,16 @@
       val node_dir = build_context.node_setup(build_dir)
 
       progress.echo("Installing rust ...")
-      platform_context.execute(build_dir, "rustup toolchain install stable").check
+      platform_context.bash("rustup toolchain install stable", cwd = build_dir).check
       if (platform.is_macos && !platform_context.apple) {
-        platform_context.execute(build_dir, "rustup target add x86_64-apple-darwin").check
+        platform_context.bash("rustup target add x86_64-apple-darwin", cwd = build_dir).check
       }
 
       progress.echo("Building VSCodium ...")
       val environment = build_context.environment(build_dir)
       progress.echo(environment, verbose = true)
-      platform_context.execute(
-        build_dir, node_dir.path_setup + "\n" + environment + "./build.sh").check
+      platform_context.bash(
+        node_dir.path_setup + "\n" + environment + "./build.sh", cwd = build_dir).check
 
       Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)