# HG changeset patch
# User wenzelm
# Date 1310842361 -7200
# Node ID 7f2cbc7133443ddfe234bb0d329db03979e24840
# Parent  00f4b305687d360d411c8acf1f4b454d02b4e0ca
moved bash operations to Isabelle_System (cf. Scala version);

diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -50,7 +50,7 @@
     (* call solver *)
     val output_file = filename dir "sos_out"
     val (output, rv) =
-      bash_output
+      Isabelle_System.bash_output
        (if File.exists exe then
           space_implode " " (map File.shell_path [exe, input_file, output_file])
         else error ("Bad executable: " ^ File.platform_path exe))
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Matrix/Compute_Oracle/am_ghc.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -227,7 +227,7 @@
         val module_file = tmp_file (module^".hs")
         val object_file = tmp_file (module^".o")
         val _ = writeTextFile module_file source
-        val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
+        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
         val _ =
           if not (fileExists object_file) then
             raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
@@ -311,7 +311,7 @@
         val term = print_term arity_of 0 t
         val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
         val _ = writeTextFile call_file call_source
-        val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
+        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
         val result = readResultFile result_file handle IO.Io _ =>
           raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
         val t' = parse_result arity_of result
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Matrix/Cplex_tools.ML
--- a/src/HOL/Matrix/Cplex_tools.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Matrix/Cplex_tools.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -1141,7 +1141,7 @@
     val cplex_path = getenv "GLPK_PATH"
     val cplex = if cplex_path = "" then "glpsol" else cplex_path
     val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
-    val answer = #1 (bash_output command)
+    val answer = #1 (Isabelle_System.bash_output command)
     in
     let
         val result = load_glpkResult resultname
@@ -1174,7 +1174,7 @@
     val cplex = if cplex_path = "" then "cplex" else cplex_path
     val _ = write_script scriptname lpname resultname
     val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
-    val answer = "return code " ^ string_of_int (bash command)
+    val answer = "return code " ^ string_of_int (Isabelle_System.bash command)
     in
     let
         val result = load_cplexResult resultname
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -13,7 +13,8 @@
   (warning "No prolog system found - skipping some example theories"; ())
 else
   if not (getenv "ISABELLE_SWIPL" = "") orelse
-    #1 (bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") = "5.10.1"
+    #1 (Isabelle_System.bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") =
+      "5.10.1"
   then
      (use_thys [
         "Code_Prolog_Examples",
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/TPTP/atp_export.ML
--- a/src/HOL/TPTP/atp_export.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -122,7 +122,7 @@
       " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
       File.shell_path prob_file
   in
-    TimeLimit.timeLimit (seconds 0.3) bash_output command
+    TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command
     |> fst
     |> extract_tstplike_proof_and_outcome false true proof_delims
                                           known_failures
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -339,7 +339,7 @@
 val systems = Synchronized.var "atp_systems" ([] : string list)
 
 fun get_systems () =
-  case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
+  case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
     (output, 0) => split_lines output
   | (output, _) =>
     error (case extract_known_failure known_perl_failures output of
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -1034,7 +1034,7 @@
           val outcome =
             let
               val code =
-                bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
+                Isabelle_System.bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
                       \\"$KODKODI\"/bin/kodkodi" ^
                       (if ms >= 0 then " -max-msecs " ^ string_of_int ms
                        else "") ^
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -792,7 +792,7 @@
   in
     if getenv env_var = "" then
       (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
-    else fst (bash_output (cmd ^ File.shell_path file))
+    else fst (Isabelle_System.bash_output (cmd ^ File.shell_path file))
   end
 
 
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -253,9 +253,10 @@
         val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ ";"
-        val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd) 
+        val (result, compilation_time) =
+          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
         val _ = Quickcheck.add_timing compilation_time current_result
-        val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
+        val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
         fun with_size k =
           if k > size then
             (NONE, !current_result)
@@ -264,7 +265,7 @@
               val _ = message ("Test data size: " ^ string_of_int k)
               val _ = current_size := k
               val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
-                (fn () => bash_output (executable ^ " " ^ string_of_int k))
+                (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
               val _ = Quickcheck.add_timing timing current_result
             in
               if response = "NONE\n" then
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -682,7 +682,7 @@
                     upto conjecture_offset + length hyp_ts + 1
                   |> map single
                 val ((output, msecs), (atp_proof, outcome)) =
-                  TimeLimit.timeLimit generous_slice_timeout bash_output command
+                  TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
                   |>> (if overlord then
                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
                        else
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -280,7 +280,7 @@
 (* ------------------------------------------------------------------------- *)
 
   fun make_external_solver cmd writefn readfn fm =
-    (writefn fm; bash cmd; readfn ());
+    (writefn fm; Isabelle_System.bash cmd; readfn ());
 
 (* ------------------------------------------------------------------------- *)
 (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
diff -r 00f4b305687d -r 7f2cbc713344 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -64,7 +64,7 @@
       val svc_output_file = File.tmp_path (Path.basic "SVM_out");
       val _ = File.write svc_input_file svc_input;
       val _ =
-        bash_output (check_valid ^ " -dump-result " ^
+        Isabelle_System.bash_output (check_valid ^ " -dump-result " ^
           File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
           ">/dev/null 2>&1")
       val svc_output =
diff -r 00f4b305687d -r 7f2cbc713344 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -4,7 +4,10 @@
 GNU bash processes, with propagation of interrupts.
 *)
 
-val bash_process = uninterruptible (fn restore_attributes => fn script =>
+structure Bash =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
   let
     datatype result = Wait | Signal | Result of int;
     val result = Synchronized.var "bash_result" Wait;
@@ -83,3 +86,5 @@
     handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
   end);
 
+end;
+
diff -r 00f4b305687d -r 7f2cbc713344 src/Pure/Concurrent/bash_ops.ML
--- a/src/Pure/Concurrent/bash_ops.ML	Sat Jul 16 20:14:58 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      Pure/Concurrent/bash_ops.ML
-    Author:     Makarius
-
-Derived operations for bash_process.
-*)
-
-fun bash_output s =
-  let val {output, rc, ...} = bash_process s
-  in (output, rc) end;
-
-fun bash s =
-  (case bash_output s of
-    ("", rc) => rc
-  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
-
diff -r 00f4b305687d -r 7f2cbc713344 src/Pure/Concurrent/bash_sequential.ML
--- a/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -5,7 +5,10 @@
 could work via the controlling tty).
 *)
 
-fun bash_process script =
+structure Bash =
+struct
+
+fun process script =
   let
     val id = serial_string ();
     val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
@@ -32,3 +35,5 @@
     handle exn => (cleanup (); reraise exn)
   end;
 
+end;
+
diff -r 00f4b305687d -r 7f2cbc713344 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/IsaMakefile	Sat Jul 16 20:52:41 2011 +0200
@@ -53,7 +53,6 @@
 
 $(OUT)/Pure: $(BOOTSTRAP_FILES)				\
   Concurrent/bash.ML 					\
-  Concurrent/bash_ops.ML				\
   Concurrent/bash_sequential.ML				\
   Concurrent/cache.ML					\
   Concurrent/future.ML					\
diff -r 00f4b305687d -r 7f2cbc713344 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -79,7 +79,6 @@
 if Multithreading.available
 then use "Concurrent/bash.ML"
 else use "Concurrent/bash_sequential.ML";
-use "Concurrent/bash_ops.ML";
 
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";
diff -r 00f4b305687d -r 7f2cbc713344 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -15,11 +15,25 @@
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   val with_tmp_fifo: (Path.T -> 'a) -> 'a
   val bash_output_stream: string -> (TextIO.instream -> 'a) -> 'a
+  val bash_output: string -> string * int
+  val bash: string -> int
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
 struct
 
+(* bash *)
+
+fun bash_output s =
+  let val {output, rc, ...} = Bash.process s
+  in (output, rc) end;
+
+fun bash s =
+  (case bash_output s of
+    ("", rc) => rc
+  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
+
+
 (* system commands *)
 
 fun isabelle_tool name args =
@@ -72,6 +86,9 @@
     val _ = mkdirs path;
   in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
 
+
+(* process output stream *)
+
 fun with_tmp_fifo f =
   with_tmp_file "isabelle-fifo-" ""
     (fn path =>
@@ -79,13 +96,10 @@
         (_, 0) => f path
       | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
 
-
-(* process output stream *)
-
 fun bash_output_stream script f =
   with_tmp_fifo (fn fifo =>
     uninterruptible (fn restore_attributes => fn () =>
-      (case bash_process (script ^ " > " ^ File.shell_path fifo ^ " &") of
+      (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
         {rc = 0, terminate, ...} =>
           Exn.release
             (Exn.capture (restore_attributes (fn () => File.open_input f fifo)) ()
diff -r 00f4b305687d -r 7f2cbc713344 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Thy/present.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -324,7 +324,7 @@
       \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
     val doc_path = Path.append result_path (Path.ext format (Path.basic name));
     val _ = if verbose then writeln s else ();
-    val (out, rc) = bash_output s;
+    val (out, rc) = Isabelle_System.bash_output s;
     val _ =
       if not (File.exists doc_path) orelse rc <> 0 then
         cat_error out ("Failed to build document " ^ quote (show_path doc_path))
diff -r 00f4b305687d -r 7f2cbc713344 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Tools/Code/code_target.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -403,11 +403,13 @@
         val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
           module_name args naming program names_cs);
         val cmd = make_command module_name;
-      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
+      in
+        if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
         else ()
       end;
-  in if getenv env_var = ""
+  in
+    if getenv env_var = ""
     then if strict
       then error (env_var ^ " not set; cannot check code for " ^ target)
       else warning (env_var ^ " not set; skipped checking code for " ^ target)
diff -r 00f4b305687d -r 7f2cbc713344 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Tools/cache_io.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -40,7 +40,7 @@
 fun raw_run make_cmd str in_path out_path =
   let
     val _ = File.write in_path str
-    val (out2, rc) = bash_output (make_cmd in_path out_path)
+    val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
     val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
   in {output=split_lines out2, redirected_output=out1, return_code=rc} end