src/Pure/General/file.ML

--- a/src/Pure/General/file.ML	Fri Jun 24 23:11:59 2022 +0200
+++ b/src/Pure/General/file.ML	Fri Jun 24 23:31:28 2022 +0200
@@ -20,22 +20,13 @@
   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_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 eq: Path.T * Path.T -> bool
@@ -93,31 +84,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
@@ -128,21 +98,15 @@
 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;
-
 (*
   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 =>
+fun fold_lines f path a = File_Stream.open_input (fn file =>
   let
     fun read buf x =
-      (case input file of
+      (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
@@ -154,17 +118,13 @@
 
 fun read_lines path = rev (fold_lines cons path []);
 
-val read = open_input input_all;
+val read = File_Stream.open_input File_Stream.input_all;
 
 
-(* 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];