src/Tools/cache_io.ML

 Cache for output of external processes.
 *)
 
 signature CACHE_IO =
 sig
-  (*IO wrapper*)
-  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> Process_Result.T
-  val run: (Path.T -> Path.T -> string) -> string -> Process_Result.T
-
-  (*cache*)
   type cache
   val unsynchronized_init: Path.T -> cache
   val cache_path_of: cache -> Path.T
   val lookup: cache -> string -> Process_Result.T option * string
-  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> Process_Result.T
-  val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> Process_Result.T
+  val run: Bash.params -> string -> Process_Result.T
+  val run_and_cache: cache -> string -> Bash.params -> string -> Process_Result.T
+  val run_cached: cache -> Bash.params -> string -> Process_Result.T
 end
 
 structure Cache_IO : CACHE_IO =
 struct
-
-(* IO wrapper *)
-
-val cache_io_prefix = "cache-io-"
-
-fun try_read_lines path =
-  let
-    fun loop n =
-      (case try File.read_lines path of
-        SOME lines => lines
-      | NONE => if n > 0 then (OS.Process.sleep (seconds 0.05); loop (n - 1)) else [])
-  in if File.exists path then loop (if ML_System.platform_is_windows then 20 else 0) else [] end
-
-fun raw_run make_cmd str in_path out_path =
-  let
-    val _ = File.write in_path str
-    val (err, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
-    val out_lines = try_read_lines out_path
-  in
-    Process_Result.make
-      {rc = rc, out_lines = out_lines, err_lines = split_lines err, timing = Timing.zero}
-  end
-
-fun run make_cmd str =
-  Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
-    Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path =>
-      raw_run make_cmd str in_path out_path))
-
-
-(* cache *)
 
 abstype cache = Cache of {
   path: Path.T,
   table: (int * (int * int * int) Symtab.table) Synchronized.var }
 with

             val result =
               Process_Result.make {rc = 0, out_lines = out, err_lines = err, timing = Timing.zero}
           in ((SOME result, key), tab) end))
   end
 
-fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
+fun run cmd input =
   let
-    val result = run make_cmd str
+    val result = cmd
+      |> Bash.input (Bytes.string input)
+      |> Bash.redirect
+      |> Isabelle_System.bash_process
+    val rc = Process_Result.rc result
+  in
+    if rc = Process_Result.startup_failure_rc then
+      Process_Result.make
+       {rc = rc,
+        err_lines = Process_Result.out_lines result,
+        out_lines = [],
+        timing = Process_Result.timing result}
+    else result
+  end
+
+fun run_and_cache (Cache {path = cache_path, table}) key cmd input =
+  let
+    val result = run cmd input
     val out_lines = Process_Result.out_lines result
     val err_lines = Process_Result.err_lines result
     val (l1, l2) = apply2 length (out_lines, err_lines)
     val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
     val lines = map (suffix "\n") (header :: out_lines @ err_lines)

       else
         let val _ = File.append_list cache_path lines
         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
   in result end
 
-fun run_cached cache make_cmd str =
-  (case lookup cache str of
-    (NONE, key) => run_and_cache cache key make_cmd str
+fun run_cached cache cmd input =
+  (case lookup cache input of
+    (NONE, key) => run_and_cache cache key cmd input
   | (SOME output, _) => output)
 
 end
 
 end