clarified modules;

--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Sat Feb 20 22:09:16 2021 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Sat Feb 20 23:01:35 2021 +0100
@@ -74,11 +74,6 @@
 | CVC4_Not_Found
 | Unknown_Error of int * string;
 
-fun bash_output_error s =
-  let val {out, err, rc, ...} = Bash.process s in
-    ((out, err), rc)
-  end;
-
 val nunchaku_home_env_var = "NUNCHAKU_HOME";
 
 val unknown_solver = "unknown";
@@ -108,7 +103,7 @@
           [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];
         val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
         val _ = File.write prob_path prob_str;
-        val ((output, error), code) = bash_output_error bash_cmd;
+        val {out = output, err = error, rc = code, ...} = Isabelle_System.bash_process bash_cmd;
 
         val backend =
           (case map_filter (try (unprefix "{backend:")) (split_lines output) of

--- a/src/Pure/General/file.ML	Sat Feb 20 22:09:16 2021 +0100
+++ b/src/Pure/General/file.ML	Sat Feb 20 23:01:35 2021 +0100
@@ -48,10 +48,10 @@
 val standard_path = Path.implode o Path.expand;
 val platform_path = ML_System.platform_path o standard_path;
 
-val bash_path = Bash_Syntax.string o standard_path;
-val bash_paths = Bash_Syntax.strings o map standard_path;
+val bash_path = Bash.string o standard_path;
+val bash_paths = Bash.strings o map standard_path;
 
-val bash_platform_path = Bash_Syntax.string o platform_path;
+val bash_platform_path = Bash.string o platform_path;
 
 
 (* full_path *)

--- a/src/Pure/ROOT.ML	Sat Feb 20 22:09:16 2021 +0100
+++ b/src/Pure/ROOT.ML	Sat Feb 20 23:01:35 2021 +0100
@@ -79,7 +79,7 @@
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";
-ML_file "System/bash_syntax.ML";
+ML_file "System/bash.ML";
 ML_file "General/file.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
@@ -294,7 +294,6 @@
 (*Isabelle system*)
 ML_file "PIDE/protocol_command.ML";
 ML_file "System/scala.ML";
-ML_file "System/bash.ML";
 ML_file "System/isabelle_system.ML";
 
 

--- a/src/Pure/System/bash.ML	Sat Feb 20 22:09:16 2021 +0100
+++ b/src/Pure/System/bash.ML	Sat Feb 20 23:01:35 2021 +0100
@@ -1,36 +1,35 @@
 (*  Title:      Pure/System/bash.ML
     Author:     Makarius
 
-GNU bash processes, with propagation of interrupts -- POSIX version.
+Syntax for GNU bash.
 *)
 
 signature BASH =
 sig
   val string: string -> string
   val strings: string list -> string
-  val process: string -> {out: string, err: string, rc: int}
 end;
 
 structure Bash: BASH =
 struct
 
-val string = Bash_Syntax.string;
-val strings = Bash_Syntax.strings;
+fun string "" = "\"\""
+  | string str =
+      str |> translate_string (fn ch =>
+        let val c = ord ch in
+          (case ch of
+            "\t" => "$'\\t'"
+          | "\n" => "$'\\n'"
+          | "\f" => "$'\\f'"
+          | "\r" => "$'\\r'"
+          | _ =>
+              if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
+                exists_string (fn c => c = ch) "+,-./:_" then ch
+              else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
+              else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
+              else "\\" ^ ch)
+        end);
 
-fun process script =
-  Scala.function_thread "bash_process"
-    ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
-  |> YXML.parse_body
-  |>
-    let open XML.Decode in
-      variant
-       [fn ([], []) => raise Exn.Interrupt,
-        fn ([], a) => error (YXML.string_of_body a),
-        fn ([a], c) =>
-          let
-            val rc = int_atom a;
-            val (out, err) = pair I I c |> apply2 YXML.string_of_body;
-          in {out = out, err = err, rc = rc} end]
-    end;
+val strings = space_implode " " o map string;
 
 end;

--- a/src/Pure/System/bash_syntax.ML	Sat Feb 20 22:09:16 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/System/bash_syntax.ML
-    Author:     Makarius
-
-Syntax for GNU bash (see also Pure/System/bash.ML).
-*)
-
-signature BASH_SYNTAX =
-sig
-  val string: string -> string
-  val strings: string list -> string
-end;
-
-structure Bash_Syntax: BASH_SYNTAX =
-struct
-
-fun string "" = "\"\""
-  | string str =
-      str |> translate_string (fn ch =>
-        let val c = ord ch in
-          (case ch of
-            "\t" => "$'\\t'"
-          | "\n" => "$'\\n'"
-          | "\f" => "$'\\f'"
-          | "\r" => "$'\\r'"
-          | _ =>
-              if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
-                exists_string (fn c => c = ch) "+,-./:_" then ch
-              else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
-              else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
-              else "\\" ^ ch)
-        end);
-
-val strings = space_implode " " o map string;
-
-end;

--- a/src/Pure/System/isabelle_system.ML	Sat Feb 20 22:09:16 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sat Feb 20 23:01:35 2021 +0100
@@ -6,6 +6,7 @@
 
 signature ISABELLE_SYSTEM =
 sig
+  val bash_process: string -> {out: string, err: string, rc: int}
   val bash_output_check: string -> string
   val bash_output: string -> string * int
   val bash: string -> int
@@ -28,14 +29,30 @@
 
 (* bash *)
 
+fun bash_process script =
+  Scala.function_thread "bash_process"
+    ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
+  |> YXML.parse_body
+  |>
+    let open XML.Decode in
+      variant
+       [fn ([], []) => raise Exn.Interrupt,
+        fn ([], a) => error (YXML.string_of_body a),
+        fn ([a], c) =>
+          let
+            val rc = int_atom a;
+            val (out, err) = pair I I c |> apply2 YXML.string_of_body;
+          in {out = out, err = err, rc = rc} end]
+    end;
+
 fun bash_output_check s =
-  (case Bash.process s of
+  (case bash_process s of
     {rc = 0, out, ...} => trim_line out
   | {err, ...} => error (trim_line err));
 
 fun bash_output s =
   let
-    val {out, err, rc, ...} = Bash.process s;
+    val {out, err, rc, ...} = bash_process s;
     val _ = warning (trim_line err);
   in (out, rc) end;
 
@@ -127,7 +144,7 @@
 fun download url =
   with_tmp_file "download" "" (fn path =>
     ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path)
-    |> Bash.process
+    |> bash_process
     |> (fn {rc = 0, ...} => File.read path
          | {err, ...} => cat_error ("Failed to download " ^ quote url) err));
 

--- a/src/Pure/Tools/ghc.ML	Sat Feb 20 22:09:16 2021 +0100
+++ b/src/Pure/Tools/ghc.ML	Sat Feb 20 23:01:35 2021 +0100
@@ -84,8 +84,9 @@
     val template_path = dir + (Path.basic name |> Path.ext "hsfiles");
     val _ = File.write template_path (project_template {depends = depends, modules = modules});
     val {rc, err, ...} =
-      Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
-        " --bare " ^ File.bash_platform_path template_path);
+      Isabelle_System.bash_process
+        ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
+          " --bare " ^ File.bash_platform_path template_path);
   in if rc = 0 then () else error err end;
 
 end;