# HG changeset patch
# User wenzelm
# Date 1656060923 -7200
# Node ID 03ae0ba2aa9e238e7f44286be3467356f6c019b4
# Parent  0f7cb6cd08fe6d1eaa695794e76f0e576c13660e
prefer scalable Bytes.T;

diff -r 0f7cb6cd08fe -r 03ae0ba2aa9e src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Import/import_rule.ML	Fri Jun 24 10:55:23 2022 +0200
@@ -441,7 +441,7 @@
   end
 
 fun process_file path thy =
-  (thy, init_state) |> File.fold_lines process_line path |> fst
+  #1 (fold process_line (Bytes.trim_split_lines (Bytes.read path)) (thy, init_state))
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
   "import a recorded proof file"
diff -r 0f7cb6cd08fe -r 03ae0ba2aa9e src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jun 24 10:55:23 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 File.read_lines #> these
+    val lines_of = Path.explode #> try (Bytes.read #> Bytes.trim_split_lines) #> these
     val liness0 = map lines_of file_names
     val num_lines = fold (Integer.max o length) liness0 0
 
diff -r 0f7cb6cd08fe -r 03ae0ba2aa9e src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jun 24 10:55:23 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 |> File.read_lines
-    val mepo_lines = Path.explode mepo_file_name |> File.read_lines
+    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
   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 0f7cb6cd08fe -r 03ae0ba2aa9e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 24 10:55:23 2022 +0200
@@ -681,7 +681,7 @@
         time_state
       else
         (disk_time,
-         (case try File.read_lines path of
+         (case try (Bytes.trim_split_lines o Bytes.read) path of
            SOME (version' :: node_lines) =>
            let
              fun extract_line_and_add_node line =