# HG changeset patch
# User wenzelm
# Date 1656106721 -7200
# Node ID 986506233812496ea38eb5f3b8813e7dfe3ab76e
# Parent  4494cd69f97faae3375aa61377cae44b499e581b
clarified signature: File.read_lines is based on scalable Bytes.T;
discontinued somewhat pointless File.fold_lines;

diff -r 4494cd69f97f -r 986506233812 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jun 24 23:31:28 2022 +0200
+++ b/src/HOL/Import/import_rule.ML	Fri Jun 24 23:38:41 2022 +0200
@@ -441,7 +441,7 @@
   end
 
 fun process_file path thy =
-  #1 (fold process_line (Bytes.trim_split_lines (Bytes.read path)) (thy, init_state))
+  #1 (fold process_line (File.read_lines path) (thy, init_state))
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
   "import a recorded proof file"
diff -r 4494cd69f97f -r 986506233812 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Jun 24 23:31:28 2022 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jun 24 23:38:41 2022 +0200
@@ -46,7 +46,7 @@
       perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
 
     val methods = "isar" :: map method_of_file_name file_names
-    val lines_of = Path.explode #> try (Bytes.read #> Bytes.trim_split_lines) #> these
+    val lines_of = Path.explode #> try File.read_lines #> these
     val liness0 = map lines_of file_names
     val num_lines = fold (Integer.max o length) liness0 0
 
diff -r 4494cd69f97f -r 986506233812 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Jun 24 23:31:28 2022 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jun 24 23:38:41 2022 +0200
@@ -316,8 +316,8 @@
         val mesh_line = encode_str name ^ ": " ^ encode_strs mesh_suggs ^ "\n"
       in File.append mesh_path mesh_line end
 
-    val mash_lines = Path.explode mash_file_name |> Bytes.read |> Bytes.trim_split_lines
-    val mepo_lines = Path.explode mepo_file_name |> Bytes.read |> Bytes.trim_split_lines
+    val mash_lines = Path.explode mash_file_name |> File.read_lines
+    val mepo_lines = Path.explode mepo_file_name |> File.read_lines
   in
     if length mash_lines = length mepo_lines then List.app do_fact (mash_lines ~~ mepo_lines)
     else warning "Skipped: MaSh file missing or out of sync with MePo file"
diff -r 4494cd69f97f -r 986506233812 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 24 23:31:28 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 24 23:38:41 2022 +0200
@@ -681,7 +681,7 @@
         time_state
       else
         (disk_time,
-         (case try (Bytes.trim_split_lines o Bytes.read) path of
+         (case try File.read_lines path of
            SOME (version' :: node_lines) =>
            let
              fun extract_line_and_add_node line =
diff -r 4494cd69f97f -r 986506233812 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Fri Jun 24 23:31:28 2022 +0200
+++ b/src/Pure/General/file.ML	Fri Jun 24 23:38:41 2022 +0200
@@ -22,9 +22,8 @@
   val check_file: Path.T -> Path.T
   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 read: Path.T -> string
   val read_lines: Path.T -> string list
-  val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
   val write_list: Path.T -> string list -> unit
@@ -98,28 +97,12 @@
 fun read_dir path = sort_strings (fold_dir cons path []);
 
 
-(*
-  scalable iterator:
-  . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
-  . optional terminator at end-of-input
-*)
-fun fold_lines f path a = File_Stream.open_input (fn file =>
-  let
-    fun read buf x =
-      (case File_Stream.input file of
-        "" => (case Buffer.content buf of "" => x | line => f line x)
-      | input =>
-          (case String.fields (fn c => c = #"\n") input of
-            [rest] => read (Buffer.add rest buf) x
-          | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
-    and read_more [rest] x = read (Buffer.add rest Buffer.empty) x
-      | read_more (line :: more) x = read_more more (f line x);
-  in read Buffer.empty a end) path;
-
-fun read_lines path = rev (fold_lines cons path []);
+(* read *)
 
 val read = File_Stream.open_input File_Stream.input_all;
 
+val read_lines = Bytes.read #> Bytes.trim_split_lines;
+
 
 (* write *)
 
diff -r 4494cd69f97f -r 986506233812 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Fri Jun 24 23:31:28 2022 +0200
+++ b/src/Tools/cache_io.ML	Fri Jun 24 23:38:41 2022 +0200
@@ -35,13 +35,11 @@
   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 read_lines out_path)
+    val out1 = the_default [] (try File.read_lines out_path)
   in {output = split_lines out2, redirected_output = out1, return_code = rc} end
 
 fun run make_cmd str =
@@ -82,7 +80,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 (fold parse (read_lines cache_path) ((1, 1), Symtab.empty)) end
+        in apfst fst (fold parse (File.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
 
@@ -100,7 +98,7 @@
               else if i < p + len2 then (i+1, apsnd (cons line) xsp)
               else (i, xsp)
             val (out, err) =
-              apply2 rev (snd (fold load (read_lines cache_path) (1, ([], []))))
+              apply2 rev (snd (fold load (File.read_lines cache_path) (1, ([], []))))
           in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
   end