--- a/src/HOL/Tools/sat_solver.ML Fri Jun 24 23:11:59 2022 +0200
+++ b/src/HOL/Tools/sat_solver.ML Fri Jun 24 23:31:28 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;
(* ------------------------------------------------------------------------- *)
--- a/src/Pure/General/bytes.ML Fri Jun 24 23:11:59 2022 +0200
+++ b/src/Pure/General/bytes.ML Fri Jun 24 23:31:28 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 *)
--- 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];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/file_stream.ML Fri Jun 24 23:31:28 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;
--- a/src/Pure/PIDE/byte_message.ML Fri Jun 24 23:11:59 2022 +0200
+++ b/src/Pure/PIDE/byte_message.ML Fri Jun 24 23:31:28 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);
--- a/src/Pure/PIDE/yxml.ML Fri Jun 24 23:11:59 2022 +0200
+++ b/src/Pure/PIDE/yxml.ML Fri Jun 24 23:31:28 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 *)
--- a/src/Pure/ROOT.ML Fri Jun 24 23:11:59 2022 +0200
+++ b/src/Pure/ROOT.ML Fri Jun 24 23:31:28 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";