# HG changeset patch
# User wenzelm
# Date 1656144343 -7200
# Node ID 85a7795675be6f8436edb71b894588d2ea68460a
# Parent  66edc020a3220f25affe09fce4516a8028e233c1# Parent  be89ec4a452323a52205c6a6923930e80d9e80ce
merged

diff -r 66edc020a322 -r 85a7795675be src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat Jun 25 10:05:43 2022 +0200
@@ -140,11 +140,12 @@
 paragraph \<open>Scopes.\<close>
 text \<open>
   Apart from very basic library modules, ML structures are not ``opened'', but
-  names are referenced with explicit qualification, as in \<^ML>\<open>Syntax.string_of_term\<close> for example. When devising names for structures and
-  their components it is important to aim at eye-catching compositions of both
-  parts, because this is how they are seen in the sources and documentation.
-  For the same reasons, aliases of well-known library functions should be
-  avoided.
+  names are referenced with explicit qualification, as in
+  \<^ML>\<open>Syntax.string_of_term\<close> for example. When devising names for
+  structures and their components it is important to aim at eye-catching
+  compositions of both parts, because this is how they are seen in the sources
+  and documentation. For the same reasons, aliases of well-known library
+  functions should be avoided.
 
   Local names of function abstraction or case/let bindings are typically
   shorter, sometimes using only rudiments of ``words'', while still avoiding
@@ -185,8 +186,10 @@
 text \<open>
   Here are some specific name forms that occur frequently in the sources.
 
-  \<^item> A function that maps \<^ML_text>\<open>foo\<close> to \<^ML_text>\<open>bar\<close> is called \<^ML_text>\<open>foo_to_bar\<close> or \<^ML_text>\<open>bar_of_foo\<close> (never \<^ML_text>\<open>foo2bar\<close>, nor
-  \<^ML_text>\<open>bar_from_foo\<close>, nor \<^ML_text>\<open>bar_for_foo\<close>, nor \<^ML_text>\<open>bar4foo\<close>).
+  \<^item> A function that maps \<^ML_text>\<open>foo\<close> to \<^ML_text>\<open>bar\<close> is called
+  \<^ML_text>\<open>foo_to_bar\<close> or \<^ML_text>\<open>bar_of_foo\<close> (never
+  \<^ML_text>\<open>foo2bar\<close>, nor \<^ML_text>\<open>bar_from_foo\<close>, nor
+  \<^ML_text>\<open>bar_for_foo\<close>, nor \<^ML_text>\<open>bar4foo\<close>).
 
   \<^item> The name component \<^ML_text>\<open>legacy\<close> means that the operation is about to
   be discontinued soon.
@@ -206,7 +209,8 @@
     \<^item> theories are called \<^ML_text>\<open>thy\<close>, rarely \<^ML_text>\<open>theory\<close>
     (never \<^ML_text>\<open>thry\<close>)
 
-    \<^item> proof contexts are called \<^ML_text>\<open>ctxt\<close>, rarely \<^ML_text>\<open>context\<close> (never \<^ML_text>\<open>ctx\<close>)
+    \<^item> proof contexts are called \<^ML_text>\<open>ctxt\<close>, rarely \<^ML_text>\<open>context\<close>
+    (never \<^ML_text>\<open>ctx\<close>)
 
     \<^item> generic contexts are called \<^ML_text>\<open>context\<close>
 
@@ -547,9 +551,10 @@
 \<close>
 
 text \<open>
-  Here the ML environment is already managed by Isabelle, i.e.\ the \<^ML>\<open>factorial\<close> function is not yet accessible in the preceding paragraph, nor in
-  a different theory that is independent from the current one in the import
-  hierarchy.
+  Here the ML environment is already managed by Isabelle, i.e.\ the
+  \<^ML>\<open>factorial\<close> function is not yet accessible in the preceding paragraph,
+  nor in a different theory that is independent from the current one in the
+  import hierarchy.
 
   Removing the above ML declaration from the source text will remove any trace
   of this definition, as expected. The Isabelle/ML toplevel environment is
@@ -583,8 +588,9 @@
   Two further ML commands are useful in certain situations: @{command_ref
   ML_val} and @{command_ref ML_command} are \<^emph>\<open>diagnostic\<close> in the sense that
   there is no effect on the underlying environment, and can thus be used
-  anywhere. The examples below produce long strings of digits by invoking \<^ML>\<open>factorial\<close>: @{command ML_val} takes care of printing the ML toplevel result,
-  but @{command ML_command} is silent so we produce an explicit output
+  anywhere. The examples below produce long strings of digits by invoking
+  \<^ML>\<open>factorial\<close>: @{command ML_val} takes care of printing the ML toplevel
+  result, but @{command ML_command} is silent so we produce an explicit output
   message.
 \<close>
 
@@ -894,9 +900,10 @@
 \<close>
 
 text \<open>
-  Note how \<^ML>\<open>fold (Buffer.add o string_of_int)\<close> above saves an extra \<^ML>\<open>map\<close> over the given list. This kind of peephole optimization reduces both
-  the code size and the tree structures in memory (``deforestation''), but it
-  requires some practice to read and write fluently.
+  Note how \<^ML>\<open>fold (Buffer.add o string_of_int)\<close> above saves an extra
+  \<^ML>\<open>map\<close> over the given list. This kind of peephole optimization reduces
+  both the code size and the tree structures in memory (``deforestation''),
+  but it requires some practice to read and write fluently.
 
   \<^medskip>
   The next example elaborates the idea of canonical iteration, demonstrating
@@ -939,10 +946,12 @@
   buffers that can be continued in further linear transformations, folding
   etc. Thus it is more compositional than the naive \<^ML>\<open>slow_content\<close>. As
   realistic example, compare the old-style
-  \<^ML>\<open>Term.maxidx_of_term: term -> int\<close> with the newer \<^ML>\<open>Term.maxidx_term: term -> int -> int\<close> in Isabelle/Pure.
+  \<^ML>\<open>Term.maxidx_of_term: term -> int\<close> with the newer
+  \<^ML>\<open>Term.maxidx_term: term -> int -> int\<close> in Isabelle/Pure.
 
   Note that \<^ML>\<open>fast_content\<close> above is only defined as example. In many
-  practical situations, it is customary to provide the incremental \<^ML>\<open>add_content\<close> only and leave the initialization and termination to the
+  practical situations, it is customary to provide the incremental
+  \<^ML>\<open>add_content\<close> only and leave the initialization and termination to the
   concrete application to the user.
 \<close>
 
@@ -1007,8 +1016,9 @@
 
   \begin{warn}
   Regular Isabelle/ML code should output messages exclusively by the official
-  channels. Using raw I/O on \<^emph>\<open>stdout\<close> or \<^emph>\<open>stderr\<close> instead (e.g.\ via \<^ML>\<open>TextIO.output\<close>) is apt to cause problems in the presence of parallel and
-  asynchronous processing of Isabelle theories. Such raw output might be
+  channels. Using raw I/O on \<^emph>\<open>stdout\<close> or \<^emph>\<open>stderr\<close> instead (e.g.\ via
+  \<^ML>\<open>TextIO.output\<close>) is apt to cause problems in the presence of parallel
+  and asynchronous processing of Isabelle theories. Such raw output might be
   displayed by the front-end in some system console log, with a low chance
   that the user will ever see it. Moreover, as a genuine side-effect on global
   process channels, there is no proper way to retract output when Isar command
@@ -1304,12 +1314,15 @@
   is mainly that of the list structure: individual symbols that happen to be a
   singleton string do not require extra memory in Poly/ML.\<close>
 
-  \<^descr> \<^ML>\<open>Symbol.is_letter\<close>, \<^ML>\<open>Symbol.is_digit\<close>, \<^ML>\<open>Symbol.is_quasi\<close>, \<^ML>\<open>Symbol.is_blank\<close> classify standard symbols
+  \<^descr> \<^ML>\<open>Symbol.is_letter\<close>, \<^ML>\<open>Symbol.is_digit\<close>,
+  \<^ML>\<open>Symbol.is_quasi\<close>, \<^ML>\<open>Symbol.is_blank\<close> classify standard symbols
   according to fixed syntactic conventions of Isabelle, cf.\ @{cite
   "isabelle-isar-ref"}.
 
   \<^descr> Type \<^ML_type>\<open>Symbol.sym\<close> is a concrete datatype that represents the
-  different kinds of symbols explicitly, with constructors \<^ML>\<open>Symbol.Char\<close>, \<^ML>\<open>Symbol.UTF8\<close>, \<^ML>\<open>Symbol.Sym\<close>, \<^ML>\<open>Symbol.Control\<close>, \<^ML>\<open>Symbol.Malformed\<close>.
+  different kinds of symbols explicitly, with constructors
+  \<^ML>\<open>Symbol.Char\<close>, \<^ML>\<open>Symbol.UTF8\<close>, \<^ML>\<open>Symbol.Sym\<close>,
+  \<^ML>\<open>Symbol.Control\<close>, \<^ML>\<open>Symbol.Malformed\<close>.
 
   \<^descr> \<^ML>\<open>Symbol.decode\<close> converts the string representation of a symbol into
   the datatype version.
@@ -1336,7 +1349,8 @@
   of its operations simply do not fit with important Isabelle/ML conventions
   (like ``canonical argument order'', see
   \secref{sec:canonical-argument-order}), others cause problems with the
-  parallel evaluation model of Isabelle/ML (such as \<^ML>\<open>TextIO.print\<close> or \<^ML>\<open>OS.Process.system\<close>).
+  parallel evaluation model of Isabelle/ML (such as \<^ML>\<open>TextIO.print\<close> or
+  \<^ML>\<open>OS.Process.system\<close>).
 
   Subsequently we give a brief overview of important operations on basic ML
   data types.
@@ -1370,7 +1384,8 @@
   Isabelle-specific purposes with the following implicit substructures packed
   into the string content:
 
-    \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with \<^ML>\<open>Symbol.explode\<close> as key operation;
+    \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with
+    \<^ML>\<open>Symbol.explode\<close> as key operation;
   
     \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), with
     \<^ML>\<open>YXML.parse_body\<close> as key operation.
@@ -1544,7 +1559,8 @@
 
 text \<open>
   Here the first list is treated conservatively: only the new elements from
-  the second list are inserted. The inside-out order of insertion via \<^ML>\<open>fold_rev\<close> attempts to preserve the order of elements in the result.
+  the second list are inserted. The inside-out order of insertion via
+  \<^ML>\<open>fold_rev\<close> attempts to preserve the order of elements in the result.
 
   This way of merging lists is typical for context data
   (\secref{sec:context-data}). See also \<^ML>\<open>merge\<close> as defined in
@@ -2128,8 +2144,9 @@
     \<^item> \<open>pri : int\<close> (default \<^ML>\<open>0\<close>) specifies a priority within the task
     queue.
 
-    Typically there is only little deviation from the default priority \<^ML>\<open>0\<close>. As a rule of thumb, \<^ML>\<open>~1\<close> means ``low priority" and \<^ML>\<open>1\<close> means
-    ``high priority''.
+    Typically there is only little deviation from the default priority
+    \<^ML>\<open>0\<close>. As a rule of thumb, \<^ML>\<open>~1\<close> means ``low priority" and
+    \<^ML>\<open>1\<close> means ``high priority''.
 
     Note that the task priority only affects the position in the queue, not
     the thread priority. When a worker thread picks up a task for processing,
@@ -2184,10 +2201,11 @@
   There is very low overhead for this proforma wrapping of strict values as
   futures.
 
-  \<^descr> \<^ML>\<open>Future.map\<close>~\<open>f x\<close> is a fast-path implementation of \<^ML>\<open>Future.fork\<close>~\<open>(fn () => f (\<close>\<^ML>\<open>Future.join\<close>~\<open>x))\<close>, which avoids the full
-  overhead of the task queue and worker-thread farm as far as possible. The
-  function \<open>f\<close> is supposed to be some trivial post-processing or projection of
-  the future result.
+  \<^descr> \<^ML>\<open>Future.map\<close>~\<open>f x\<close> is a fast-path implementation of
+  \<^ML>\<open>Future.fork\<close>~\<open>(fn () => f (\<close>\<^ML>\<open>Future.join\<close>~\<open>x))\<close>, which avoids
+  the full overhead of the task queue and worker-thread farm as far as
+  possible. The function \<open>f\<close> is supposed to be some trivial post-processing or
+  projection of the future result.
 
   \<^descr> \<^ML>\<open>Future.cancel\<close>~\<open>x\<close> cancels the task group of the given future, using
   \<^ML>\<open>Future.cancel_group\<close> below.
diff -r 66edc020a322 -r 85a7795675be src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/HOL/Import/import_rule.ML	Sat Jun 25 10:05:43 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 (File.read_lines path) (thy, init_state))
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
   "import a recorded proof file"
diff -r 66edc020a322 -r 85a7795675be src/HOL/TPTP/mash_eval.ML
diff -r 66edc020a322 -r 85a7795675be src/HOL/TPTP/mash_export.ML
diff -r 66edc020a322 -r 85a7795675be src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
diff -r 66edc020a322 -r 85a7795675be src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -129,32 +129,32 @@
           error "formula is not in CNF"
         | write_formula (BoolVar i) =
           (i>=1 orelse error "formula contains a variable index less than 1";
-           File.output out (string_of_int i))
+           File_Stream.output out (string_of_int i))
         | write_formula (Not (BoolVar i)) =
-          (File.output out "-";
+          (File_Stream.output out "-";
            write_formula (BoolVar i))
         | write_formula (Not _) =
           error "formula is not in CNF"
         | write_formula (Or (fm1, fm2)) =
           (write_formula fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula fm2)
         | write_formula (And (fm1, fm2)) =
           (write_formula fm1;
-           File.output out " 0\n";
+           File_Stream.output out " 0\n";
            write_formula fm2)
       val fm'               = cnf_True_False_elim fm
       val number_of_vars    = maxidx fm'
       val number_of_clauses = cnf_number_of_clauses fm'
     in
-      File.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n";
-      File.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^
+      File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n";
+      File_Stream.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^
                             string_of_int number_of_clauses ^ "\n");
       write_formula fm';
-      File.output out " 0\n"
+      File_Stream.output out " 0\n"
     end
   in
-    File.open_output write_cnf_file path
+    File_Stream.open_output write_cnf_file path
   end;
 
 (* ------------------------------------------------------------------------- *)
@@ -169,54 +169,54 @@
     fun write_sat_file out =
     let
       fun write_formula True =
-          File.output out "*()"
+          File_Stream.output out "*()"
         | write_formula False =
-          File.output out "+()"
+          File_Stream.output out "+()"
         | write_formula (BoolVar i) =
           (i>=1 orelse error "formula contains a variable index less than 1";
-           File.output out (string_of_int i))
+           File_Stream.output out (string_of_int i))
         | write_formula (Not (BoolVar i)) =
-          (File.output out "-";
+          (File_Stream.output out "-";
            write_formula (BoolVar i))
         | write_formula (Not fm) =
-          (File.output out "-(";
+          (File_Stream.output out "-(";
            write_formula fm;
-           File.output out ")")
+           File_Stream.output out ")")
         | write_formula (Or (fm1, fm2)) =
-          (File.output out "+(";
+          (File_Stream.output out "+(";
            write_formula_or fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_or fm2;
-           File.output out ")")
+           File_Stream.output out ")")
         | write_formula (And (fm1, fm2)) =
-          (File.output out "*(";
+          (File_Stream.output out "*(";
            write_formula_and fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_and fm2;
-           File.output out ")")
+           File_Stream.output out ")")
       (* optimization to make use of n-ary disjunction/conjunction *)
       and write_formula_or (Or (fm1, fm2)) =
           (write_formula_or fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_or fm2)
         | write_formula_or fm =
           write_formula fm
       and write_formula_and (And (fm1, fm2)) =
           (write_formula_and fm1;
-           File.output out " ";
+           File_Stream.output out " ";
            write_formula_and fm2)
         | write_formula_and fm =
           write_formula fm
       val number_of_vars = Int.max (maxidx fm, 1)
     in
-      File.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n";
-      File.output out ("p sat " ^ string_of_int number_of_vars ^ "\n");
-      File.output out "(";
+      File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n";
+      File_Stream.output out ("p sat " ^ string_of_int number_of_vars ^ "\n");
+      File_Stream.output out "(";
       write_formula fm;
-      File.output out ")\n"
+      File_Stream.output out ")\n"
     end
   in
-    File.open_output write_sat_file path
+    File_Stream.open_output write_sat_file path
   end;
 
 (* ------------------------------------------------------------------------- *)
diff -r 66edc020a322 -r 85a7795675be src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/Pure/General/bytes.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -194,7 +194,7 @@
 (* IO *)
 
 fun read_block limit =
-  File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
+  File_Stream.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
 
 fun read_stream limit stream =
   let
@@ -205,11 +205,11 @@
   in read empty end;
 
 fun write_stream stream bytes =
-  File.outputs stream (contents bytes);
+  File_Stream.outputs stream (contents bytes);
 
-fun read path = File.open_input (fn stream => read_stream ~1 stream) path;
+fun read path = File_Stream.open_input (fn stream => read_stream ~1 stream) path;
 
-fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path;
+fun write path bytes = File_Stream.open_output (fn stream => write_stream stream bytes) path;
 
 
 (* ML pretty printing *)
diff -r 66edc020a322 -r 85a7795675be src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/Pure/General/file.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -20,25 +20,14 @@
   val is_file: Path.T -> bool
   val check_dir: Path.T -> Path.T
   val check_file: Path.T -> Path.T
-  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
-  val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a
-  val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a
-  val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a
   val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read_dir: Path.T -> string list
-  val input: BinIO.instream -> string
-  val input_size: int -> BinIO.instream -> string
-  val input_all: BinIO.instream -> string
-  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 output: BinIO.outstream -> string -> unit
-  val outputs: BinIO.outstream -> string list -> unit
   val write_list: Path.T -> string list -> unit
   val append_list: Path.T -> string list -> unit
-  val write_buffer: Path.T -> Buffer.T -> unit
   val eq: Path.T * Path.T -> bool
 end;
 
@@ -94,31 +83,10 @@
   else error ("No such file: " ^ Path.print (Path.expand path));
 
 
-(* open streams *)
-
-local
-
-fun with_file open_file close_file f =
-  Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
-    let
-      val file = open_file path;
-      val result = Exn.capture (restore_attributes f) file;
-    in close_file file; Exn.release result end);
-
-in
-
-fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
-fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path;
-fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path;
-fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path;
-
-end;
-
-
 (* directory content *)
 
 fun fold_dir f path a =
-  check_dir path |> open_dir (fn stream =>
+  check_dir path |> File_Stream.open_dir (fn stream =>
     let
       fun read x =
         (case OS.FileSys.readDir stream of
@@ -129,50 +97,21 @@
 fun read_dir path = sort_strings (fold_dir cons path []);
 
 
-(* input *)
-
-val input = Byte.bytesToString o BinIO.input;
-fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n));
-val input_all = Byte.bytesToString o BinIO.inputAll;
+(* read *)
 
-(*
-  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 = open_input (fn file =>
-  let
-    fun read buf x =
-      (case 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;
+val read = File_Stream.open_input File_Stream.input_all;
 
-fun read_lines path = rev (fold_lines cons path []);
-
-val read = open_input input_all;
+val read_lines = Bytes.read #> Bytes.trim_split_lines;
 
 
-(* output *)
+(* write *)
 
-fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
-val outputs = List.app o output;
-
-fun output_list txts file = List.app (output file) txts;
-fun write_list path txts = open_output (output_list txts) path;
-fun append_list path txts = open_append (output_list txts) path;
+fun write_list path ss = File_Stream.open_output (fn stream => File_Stream.outputs stream ss) path;
+fun append_list path ss = File_Stream.open_append (fn stream => File_Stream.outputs stream ss) path;
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
 
-fun write_buffer path buf =
-  open_output (fn file => List.app (output file) (Buffer.contents buf)) path;
-
 
 (* eq *)
 
diff -r 66edc020a322 -r 85a7795675be src/Pure/General/file_stream.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/file_stream.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -0,0 +1,58 @@
+(*  Title:      Pure/General/file_stream.ML
+    Author:     Makarius
+
+File-system stream operations.
+*)
+
+signature FILE_STREAM =
+sig
+  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
+  val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a
+  val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a
+  val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a
+  val input: BinIO.instream -> string
+  val input_size: int -> BinIO.instream -> string
+  val input_all: BinIO.instream -> string
+  val output: BinIO.outstream -> string -> unit
+  val outputs: BinIO.outstream -> string list -> unit
+end;
+
+structure File_Stream: FILE_STREAM =
+struct
+
+(* open streams *)
+
+local
+
+val platform_path = ML_System.platform_path o Path.implode o Path.expand;
+
+fun with_file open_file close_file f =
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
+    let
+      val file = open_file path;
+      val result = Exn.capture (restore_attributes f) file;
+    in close_file file; Exn.release result end);
+
+in
+
+fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
+fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path;
+fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path;
+fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path;
+
+end;
+
+
+(* input *)
+
+val input = Byte.bytesToString o BinIO.input;
+fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n));
+val input_all = Byte.bytesToString o BinIO.inputAll;
+
+
+(* output *)
+
+fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
+val outputs = List.app o output;
+
+end;
diff -r 66edc020a322 -r 85a7795675be src/Pure/PIDE/byte_message.ML
--- a/src/Pure/PIDE/byte_message.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/Pure/PIDE/byte_message.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -29,7 +29,8 @@
 
 val write = List.app o Bytes.write_stream;
 
-fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree ();
+fun write_yxml stream tree =
+  YXML.traverse (fn s => fn () => File_Stream.output stream s) tree ();
 
 fun flush stream = ignore (try BinIO.flushOut stream);
 
diff -r 66edc020a322 -r 85a7795675be src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -89,8 +89,8 @@
 val string_of = string_of_body o single;
 
 fun write_body path body =
-  path |> File.open_output (fn file =>
-    fold (traverse (fn s => fn () => File.output file s)) body ());
+  path |> File_Stream.open_output (fn file =>
+    fold (traverse (fn s => fn () => File_Stream.output file s)) body ());
 
 
 (* markup elements *)
diff -r 66edc020a322 -r 85a7795675be src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/Pure/ROOT.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -78,8 +78,9 @@
 ML_file "General/path.ML";
 ML_file "General/url.ML";
 ML_file "System/bash.ML";
+ML_file "General/file_stream.ML";
+ML_file "General/bytes.ML";
 ML_file "General/file.ML";
-ML_file "General/bytes.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";
diff -r 66edc020a322 -r 85a7795675be src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Sat Jun 25 06:34:11 2022 +0200
+++ b/src/Tools/cache_io.ML	Sat Jun 25 10:05:43 2022 +0200
@@ -39,7 +39,7 @@
   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 File.read_lines out_path)
   in {output = split_lines out2, redirected_output = out1, return_code = rc} end
 
 fun run make_cmd str =
@@ -80,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 (File.fold_lines parse 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
 
@@ -98,7 +98,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 (File.read_lines cache_path) (1, ([], []))))
           in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
   end