merged
authorhaftmann
Sun, 17 Jul 2011 08:45:06 +0200
changeset 43855 01b13e9a1a7e
parent 43851 f7f8cf0a1536 (diff)
parent 43854 f1d23df1adde (current diff)
child 43856 d636b053d4ff
child 43865 db18f4d0cc7d
merged
--- a/Admin/isatest/settings/at-poly-test	Sat Jul 16 22:28:35 2011 +0200
+++ b/Admin/isatest/settings/at-poly-test	Sun Jul 17 08:45:06 2011 +0200
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
   POLYML_HOME="/home/polyml/polyml-svn"
-  ML_SYSTEM="polyml-5.4.1"
+  ML_SYSTEM="polyml-5.4.2"
   ML_PLATFORM="x86-linux"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 500"
--- a/Admin/isatest/settings/cygwin-poly-e	Sat Jul 16 22:28:35 2011 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e	Sun Jul 17 08:45:06 2011 +0200
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
   POLYML_HOME="/home/isatest/polyml-svn"
-  ML_SYSTEM="polyml-5.4.1"
+  ML_SYSTEM="polyml-5.4.2"
   ML_PLATFORM="x86-cygwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 200"
--- a/Admin/isatest/settings/mac-poly64-M4	Sat Jul 16 22:28:35 2011 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4	Sun Jul 17 08:45:06 2011 +0200
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
   POLYML_HOME="/home/polyml/polyml-svn"
-  ML_SYSTEM="polyml-5.4.1"
+  ML_SYSTEM="polyml-5.4.2"
   ML_PLATFORM="x86_64-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 2000 --gcthreads 4"
--- a/Admin/isatest/settings/mac-poly64-M8	Sat Jul 16 22:28:35 2011 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8	Sun Jul 17 08:45:06 2011 +0200
@@ -1,7 +1,7 @@
 # -*- shell-script -*- :mode=shellscript:
 
   POLYML_HOME="/home/polyml/polyml-svn"
-  ML_SYSTEM="polyml-5.4.1"
+  ML_SYSTEM="polyml-5.4.2"
   ML_PLATFORM="x86_64-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 2000 --gcthreads 4"
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sun Jul 17 08:45:06 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))
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sun Jul 17 08:45:06 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
--- a/src/HOL/Matrix/Cplex_tools.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Matrix/Cplex_tools.ML	Sun Jul 17 08:45:06 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
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sun Jul 17 08:45:06 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",
--- a/src/HOL/TPTP/atp_export.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Sun Jul 17 08:45:06 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
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Jul 17 08:45:06 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
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sun Jul 17 08:45:06 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 "") ^
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Jul 17 08:45:06 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
 
 
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Jul 17 08:45:06 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 08:45:06 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
--- a/src/HOL/Tools/sat_solver.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sun Jul 17 08:45:06 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 *)
--- a/src/HOL/ex/svc_funcs.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Sun Jul 17 08:45:06 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 =
--- a/src/Pure/Concurrent/bash.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -4,7 +4,10 @@
 GNU bash processes, with propagation of interrupts.
 *)
 
-val bash_output = 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;
@@ -39,7 +42,9 @@
           handle exn =>
             (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
 
-    fun terminate () =
+    fun get_pid () = Int.fromString (File.read pid_path) handle IO.Io _ => NONE;
+
+    fun terminate opt_pid =
       let
         val sig_test = Posix.Signal.fromWord 0w0;
 
@@ -49,10 +54,9 @@
           handle OS.SysErr _ => false;
 
         fun kill s =
-          (case Int.fromString (File.read pid_path) of
+          (case opt_pid of
             NONE => true
-          | SOME pid => (kill_group pid s; kill_group pid sig_test))
-          handle IO.Io _ => true;
+          | SOME pid => (kill_group pid s; kill_group pid sig_test));
 
         fun multi_kill count s =
           count = 0 orelse
@@ -76,8 +80,11 @@
 
       val output = the_default "" (try File.read output_path);
       val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+      val pid = get_pid ();
       val _ = cleanup ();
-    in (output, rc) end
-    handle exn => (terminate(); cleanup (); reraise exn)
+    in {output = output, rc = rc, terminate = fn () => terminate pid} end
+    handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
   end);
 
+end;
+
--- a/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -5,7 +5,10 @@
 could work via the controlling tty).
 *)
 
-fun bash_output script =
+structure Bash =
+struct
+
+fun process script =
   let
     val id = serial_string ();
     val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
@@ -28,7 +31,9 @@
 
       val output = the_default "" (try File.read output_path);
       val _ = cleanup ();
-    in (output, rc) end
+    in {output = output, rc = rc, terminate = fn () => ()} end
     handle exn => (cleanup (); reraise exn)
   end;
 
+end;
+
--- a/src/Pure/General/file.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/General/file.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -18,10 +18,15 @@
   val is_dir: Path.T -> bool
   val check_dir: Path.T -> Path.T
   val check_file: Path.T -> Path.T
+  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
+  val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
+  val read_dir: Path.T -> string list
   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
+  val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
+  val read_lines: Path.T -> string list
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
@@ -90,7 +95,7 @@
   else error ("No such file: " ^ Path.print path);
 
 
-(* open files *)
+(* open streams *)
 
 local
 
@@ -100,6 +105,7 @@
 
 in
 
+fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
 fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path;
 fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path;
 fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path;
@@ -107,22 +113,40 @@
 end;
 
 
+(* directory content *)
+
+fun fold_dir f path a = open_dir (fn stream =>
+  let
+    fun read x =
+      (case OS.FileSys.readDir stream of
+        NONE => x
+      | SOME entry => read (f entry x));
+  in read a end) path;
+
+fun read_dir path = rev (fold_dir cons path []);
+
+
 (* input *)
 
 (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
-fun fold_lines f path a = open_input (fn file =>
+fun fold_chunks terminator f path a = open_input (fn file =>
   let
     fun read buf x =
       (case TextIO.input file of
         "" => (case Buffer.content buf of "" => x | line => f line x)
       | input =>
-          (case String.fields (fn c => c = #"\n") input of
+          (case String.fields (fn c => c = terminator) input of
             [rest] => read (Buffer.add rest buf) x
           | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
     and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
       | read_lines (line :: more) x = read_lines more (f line x);
   in read Buffer.empty a end) path;
 
+fun fold_lines f = fold_chunks #"\n" f;
+fun fold_pages f = fold_chunks #"\f" f;
+
+fun read_lines path = rev (fold_lines cons path []);
+
 val read = open_input TextIO.inputAll;
 
 
--- a/src/Pure/General/symbol.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/General/symbol.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -151,7 +151,7 @@
   | is_ascii_quasi _ = false;
 
 val is_ascii_blank =
-  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
+  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true
     | _ => false;
 
 fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
--- a/src/Pure/General/xml.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/General/xml.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -310,9 +310,10 @@
   | node t = raise XML_BODY [t];
 
 fun vector atts =
-  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts;
+  #1 (fold_map (fn (a, x) =>
+        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
 
-fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
+fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   | tagged t = raise XML_BODY [t];
 
 
--- a/src/Pure/ML/ml_syntax.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -64,6 +64,7 @@
   else if s = "\\" then "\\\\"
   else if s = "\t" then "\\t"
   else if s = "\n" then "\\n"
+  else if s = "\f" then "\\f"
   else if s = "\r" then "\\r"
   else
     let val c = ord s in
--- a/src/Pure/ROOT.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/ROOT.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -80,11 +80,6 @@
 then use "Concurrent/bash.ML"
 else use "Concurrent/bash_sequential.ML";
 
-fun bash s =
-  (case bash_output s of
-    ("", rc) => rc
-  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
-
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
--- a/src/Pure/System/isabelle_system.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sun Jul 17 08:45:06 2011 +0200
@@ -13,11 +13,27 @@
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
+  val with_tmp_fifo: (Path.T -> 'a) -> 'a
+  val bash_output_fifo: string -> (Path.T -> '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 =
@@ -70,5 +86,23 @@
     val _ = mkdirs path;
   in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
 
+
+(* fifo *)
+
+fun with_tmp_fifo f =
+  with_tmp_file "isabelle-fifo-" ""
+    (fn path =>
+      (case bash_output ("mkfifo -m 600 " ^ File.shell_path path) of
+        (_, 0) => f path
+      | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
+
+fun bash_output_fifo script f =
+  with_tmp_fifo (fn fifo =>
+    uninterruptible (fn restore_attributes => fn () =>
+      (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
+        {rc = 0, terminate, ...} =>
+          (restore_attributes f fifo handle exn => (terminate (); reraise exn))
+      | {output, ...} => error (perhaps (try (unsuffix "\n")) output))) ());
+
 end;
 
--- a/src/Pure/Thy/present.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Pure/Thy/present.ML	Sun Jul 17 08:45:06 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))
--- a/src/Tools/Code/code_target.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Tools/Code/code_target.ML	Sun Jul 17 08:45:06 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)
--- a/src/Tools/cache_io.ML	Sat Jul 16 22:28:35 2011 +0200
+++ b/src/Tools/cache_io.ML	Sun Jul 17 08:45:06 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