# HG changeset patch
# User wenzelm
# Date 1619382795 -7200
# Node ID 51b291ae3e2d625028c6084a70dffcf3fa53c008
# Parent  342362c9496c33a6337472a953dca6acf5c09b50
avoid "exec" to change the winpid;

diff -r 342362c9496c -r 51b291ae3e2d lib/Tools/env
--- a/lib/Tools/env	Sun Apr 25 21:12:59 2021 +0200
+++ b/lib/Tools/env	Sun Apr 25 22:33:15 2021 +0200
@@ -25,4 +25,4 @@
 
 [ "$1" = "-?" ] && usage
 
-exec /usr/bin/env "$@"
+/usr/bin/env "$@"
diff -r 342362c9496c -r 51b291ae3e2d src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Apr 25 21:12:59 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Apr 25 22:33:15 2021 +0200
@@ -271,7 +271,7 @@
                 let val {output, timing} = SystemOnTPTP.run_system_encoded args
                 in (output, timing) end
               else
-                let val res = Isabelle_System.bash_process ("exec 2>&1; " ^ command)
+                let val res = Isabelle_System.bash_process_redirect command
                 in (Process_Result.out res, Process_Result.timing_elapsed res) end
 
             val _ =
diff -r 342362c9496c -r 51b291ae3e2d src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sun Apr 25 21:12:59 2021 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun Apr 25 22:33:15 2021 +0200
@@ -124,7 +124,7 @@
       use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
 
     Bash.process(
-      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
+      options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
         Bash.strings(bash_args),
       cwd = cwd,
       env = env ++ env_options ++ env_tmp ++ env_functions,
diff -r 342362c9496c -r 51b291ae3e2d src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sun Apr 25 21:12:59 2021 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Sun Apr 25 22:33:15 2021 +0200
@@ -70,7 +70,7 @@
     val env_prefix =
       if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
 
-    Bash.process(env_prefix + "exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
+    Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
         Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
           ML_Syntax.print_double(delay.seconds)),
         cwd = Path.ISABELLE_HOME.file)
diff -r 342362c9496c -r 51b291ae3e2d src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sun Apr 25 21:12:59 2021 +0200
+++ b/src/Pure/System/bash.scala	Sun Apr 25 22:33:15 2021 +0200
@@ -236,7 +236,12 @@
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] =
     {
-      val result = Exn.capture { Isabelle_System.bash(cat_lines(args)) }
+      val result =
+        Exn.capture {
+          val redirect = args.head == "true"
+          val script = cat_lines(args.tail)
+          Isabelle_System.bash(script, redirect = redirect)
+        }
 
       val is_interrupt =
         result match {
diff -r 342362c9496c -r 51b291ae3e2d src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sun Apr 25 21:12:59 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sun Apr 25 22:33:15 2021 +0200
@@ -7,6 +7,7 @@
 signature ISABELLE_SYSTEM =
 sig
   val bash_process: string -> Process_Result.T
+  val bash_process_redirect: string -> Process_Result.T
   val bash_output: string -> string * int
   val bash: string -> int
   val bash_functions: unit -> string list
@@ -34,9 +35,9 @@
 
 (* bash *)
 
-fun bash_process script =
+fun invoke_bash_process redirect script =
   Scala.function "bash_process"
-    ["export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
+    [Value.print_bool redirect, "export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
   |> (fn [] => raise Exn.Interrupt
       | [err] => error err
       | a :: b :: c :: d :: lines =>
@@ -53,6 +54,9 @@
          end
       | _ => raise Fail "Malformed Isabelle/Scala result");
 
+val bash_process = invoke_bash_process false;
+val bash_process_redirect = invoke_bash_process true;
+
 val bash = bash_process #> Process_Result.print #> Process_Result.rc;
 
 fun bash_output s =