# HG changeset patch
# User wenzelm
# Date 1656105119 -7200
# Node ID 01b3da984e55b99f8e31fe666e28d67e387f199d
# Parent  1b50bcd108b75485a727e5062e4d691f4cfbce8e
prefer scalable Bytes.T;

diff -r 1b50bcd108b7 -r 01b3da984e55 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Fri Jun 24 11:20:14 2022 +0200
+++ b/src/Tools/cache_io.ML	Fri Jun 24 23:11:59 2022 +0200
@@ -35,11 +35,13 @@
   redirected_output: string list,
   return_code: int}
 
+val read_lines = Bytes.read #> Bytes.trim_split_lines
+
 fun raw_run make_cmd str in_path out_path =
   let
     val _ = File.write in_path str
     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) [])
+    val out1 = the_default [] (try read_lines out_path)
   in {output = split_lines out2, redirected_output = out1, return_code = rc} end
 
 fun run make_cmd str =
@@ -80,7 +82,7 @@
               let val (key, l1, l2) = split line
               in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
             else ((i+1, l), tab)
-        in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
+        in apfst fst (fold parse (read_lines cache_path) ((1, 1), Symtab.empty)) end
       else (1, Symtab.empty)
   in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end
 
@@ -98,7 +100,7 @@
               else if i < p + len2 then (i+1, apsnd (cons line) xsp)
               else (i, xsp)
             val (out, err) =
-              apply2 rev (snd (File.fold_lines load cache_path (1, ([], []))))
+              apply2 rev (snd (fold load (read_lines cache_path) (1, ([], []))))
           in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
   end