# HG changeset patch
# User wenzelm
# Date 1717245218 -7200
# Node ID af6b60c75d7d95095ff473f99cbf3e74cb67311a
# Parent  17a10bea79a1f5d83edfd954495373895eb91995
clarified context for (remote) bash scripts: export variables are optional, support cwd;

diff -r 17a10bea79a1 -r af6b60c75d7d src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Jun 01 14:08:04 2024 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jun 01 14:33:38 2024 +0200
@@ -221,9 +221,9 @@
         settings: Boolean = true,  // ignored
         cleanup: () => Unit = () => ()
     ): Bash.Process = {
-      val remote_script1 = Isabelle_System.export_env(user_home = user_home) + remote_script
-      Bash.process(remote_script1, description = description, cwd = cwd, redirect = redirect,
-        cleanup = cleanup, ssh = ssh)
+      Bash.process(
+        Bash.context(remote_script, user_home = user_home),
+        description = description, cwd = cwd, redirect = redirect, cleanup = cleanup, ssh = ssh)
     }
 
     override def execute(remote_script: String,
@@ -233,8 +233,11 @@
       settings: Boolean = true,  // ignored
       strict: Boolean = true
     ): Process_Result = {
-      val remote_script1 = Isabelle_System.export_env(user_home = user_home) + remote_script
-      Isabelle_System.bash(make_command(args_host = true, args = Bash.string(remote_script1)),
+      val script =
+        make_command(
+          args_host = true,
+          args = Bash.string(Bash.context(remote_script, user_home = user_home)))
+      Isabelle_System.bash(script,
         progress_stdout = progress_stdout,
         progress_stderr = progress_stderr,
         redirect = redirect,
diff -r 17a10bea79a1 -r af6b60c75d7d src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Jun 01 14:08:04 2024 +0200
+++ b/src/Pure/System/bash.scala	Sat Jun 01 14:33:38 2024 +0200
@@ -45,6 +45,19 @@
 
   /* process and result */
 
+  def context(script: String,
+    user_home: String = "",
+    isabelle_identifier: String = "",
+    cwd: Path = Path.current
+  ): String = {
+    if_proper(user_home,
+      "export USER_HOME=" + Bash.string(user_home) + "\n") +
+    if_proper(isabelle_identifier,
+      "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n") +
+    (if (cwd == null || cwd.is_current) "" else "cd " + quote(cwd.implode) + "\n") +
+    script
+  }
+
   private def make_description(description: String): String =
     proper_string(description) getOrElse "bash_process"
 
diff -r 17a10bea79a1 -r af6b60c75d7d src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jun 01 14:08:04 2024 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 01 14:33:38 2024 +0200
@@ -117,10 +117,6 @@
       else ""
     }
 
-  def export_env(user_home: String = "", isabelle_identifier: String = ""): String =
-    "export USER_HOME=" + Bash.string(user_home) + "\n" +
-    "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
-
   def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
 
   def isabelle_heading(): String =
diff -r 17a10bea79a1 -r af6b60c75d7d src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Sat Jun 01 14:08:04 2024 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sat Jun 01 14:33:38 2024 +0200
@@ -43,17 +43,19 @@
 
   /* static system */
 
+  def bash_context(script: String): String =
+    Bash.context(script,
+      user_home = ssh.user_home,
+      isabelle_identifier = isabelle_identifier,
+      cwd = isabelle_home)
+
   def bash(
     script: String,
     redirect: Boolean = false,
     echo: Boolean = false,
     strict: Boolean = true
   ): Process_Result = {
-    val env =
-      Isabelle_System.export_env(
-        user_home = ssh.user_home,
-        isabelle_identifier = isabelle_identifier)
-    ssh.execute(env + "cd " + ssh.bash_path(isabelle_home) + "\n" + script,
+    ssh.execute(bash_context(script),
       progress_stdout = progress.echo_if(echo, _),
       progress_stderr = progress.echo_if(echo, _),
       redirect = redirect,