src/Tools/cache_io.ML

   val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result
   val run: (Path.T -> Path.T -> string) -> string -> result
 
   (*cache*)
   type cache
-  val make: Path.T -> cache
+  val unsynchronized_init: Path.T -> cache
   val cache_path_of: cache -> Path.T
   val lookup: cache -> string -> result option * string
   val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
   val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
 end

   table: (int * (int * int * int) Symtab.table) Synchronized.var }
 with
 
 fun cache_path_of (Cache {path, ...}) = path
 
-fun make cache_path =
+fun unsynchronized_init cache_path =
   let
     val table =
       if File.exists cache_path then
         let
           fun err () = error ("Cache IO: corrupted cache file: " ^ File.shell_path cache_path)

             else ((i+1, l), tab)
         in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
       else (1, Symtab.empty)
   in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end
 
-fun load_cached_result cache_path (p, len1, len2) =
-  let
-    fun load line (i, xsp) =
-      if i < p then (i+1, xsp)
-      else if i < p + len1 then (i+1, apfst (cons line) xsp)
-      else if i < p + len2 then (i+1, apsnd (cons line) xsp)
-      else (i, xsp)
-    val (out, err) =
-      pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
-  in {output = err, redirected_output = out, return_code = 0} end
-
 fun lookup (Cache {path = cache_path, table}) str =
   let val key = SHA1.rep (SHA1.digest str)
   in
-    (case Symtab.lookup (snd (Synchronized.value table)) key of
-      NONE => (NONE, key)
-    | SOME pos => (SOME (load_cached_result cache_path pos), key))
+    Synchronized.change_result table (fn tab =>
+      (case Symtab.lookup (snd tab) key of
+        NONE => ((NONE, key), tab)
+      | SOME (p, len1, len2) =>
+          let
+            fun load line (i, xsp) =
+              if i < p then (i+1, xsp)
+              else if i < p + len1 then (i+1, apfst (cons line) xsp)
+              else if i < p + len2 then (i+1, apsnd (cons line) xsp)
+              else (i, xsp)
+            val (out, err) =
+              pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
+          in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
   end
 
 fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
   let
     val {output = err, redirected_output=out, return_code} = run make_cmd str