--- a/src/HOL/TPTP/TPTP_Parser/tptp_parser.ML Wed Aug 19 22:40:41 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_parser.ML Thu Aug 20 13:41:53 2015 +0200
@@ -65,7 +65,7 @@
fun parse_file' lookahead file_name =
parse_expression
file_name
- (File.open_input TextIO.inputAll (Path.explode file_name))
+ (File.read (Path.explode file_name))
end
val parse_file = parse_file' LOOKAHEAD
--- a/src/HOL/Tools/sat_solver.ML Wed Aug 19 22:40:41 2015 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu Aug 20 13:41:53 2015 +0200
@@ -129,29 +129,29 @@
error "formula is not in CNF"
| write_formula (BoolVar i) =
(i>=1 orelse error "formula contains a variable index less than 1";
- TextIO.output (out, string_of_int i))
+ File.output out (string_of_int i))
| write_formula (Not (BoolVar i)) =
- (TextIO.output (out, "-");
+ (File.output out "-";
write_formula (BoolVar i))
| write_formula (Not _) =
error "formula is not in CNF"
| write_formula (Or (fm1, fm2)) =
(write_formula fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula fm2)
| write_formula (And (fm1, fm2)) =
(write_formula fm1;
- TextIO.output (out, " 0\n");
+ File.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
- TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n");
- TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^
+ 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 ^ " " ^
string_of_int number_of_clauses ^ "\n");
write_formula fm';
- TextIO.output (out, " 0\n")
+ File.output out " 0\n"
end
in
File.open_output write_cnf_file path
@@ -169,51 +169,51 @@
fun write_sat_file out =
let
fun write_formula True =
- TextIO.output (out, "*()")
+ File.output out "*()"
| write_formula False =
- TextIO.output (out, "+()")
+ File.output out "+()"
| write_formula (BoolVar i) =
(i>=1 orelse error "formula contains a variable index less than 1";
- TextIO.output (out, string_of_int i))
+ File.output out (string_of_int i))
| write_formula (Not (BoolVar i)) =
- (TextIO.output (out, "-");
+ (File.output out "-";
write_formula (BoolVar i))
| write_formula (Not fm) =
- (TextIO.output (out, "-(");
+ (File.output out "-(";
write_formula fm;
- TextIO.output (out, ")"))
+ File.output out ")")
| write_formula (Or (fm1, fm2)) =
- (TextIO.output (out, "+(");
+ (File.output out "+(";
write_formula_or fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_or fm2;
- TextIO.output (out, ")"))
+ File.output out ")")
| write_formula (And (fm1, fm2)) =
- (TextIO.output (out, "*(");
+ (File.output out "*(";
write_formula_and fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_and fm2;
- TextIO.output (out, ")"))
+ File.output out ")")
(* optimization to make use of n-ary disjunction/conjunction *)
and write_formula_or (Or (fm1, fm2)) =
(write_formula_or fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_or fm2)
| write_formula_or fm =
write_formula fm
and write_formula_and (And (fm1, fm2)) =
(write_formula_and fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_and fm2)
| write_formula_and fm =
write_formula fm
val number_of_vars = Int.max (maxidx fm, 1)
in
- TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_sat_file\n");
- TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n");
- TextIO.output (out, "(");
+ 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 "(";
write_formula fm;
- TextIO.output (out, ")\n")
+ File.output out ")\n"
end
in
File.open_output write_sat_file path
--- a/src/Pure/General/buffer.ML Wed Aug 19 22:40:41 2015 +0200
+++ b/src/Pure/General/buffer.ML Thu Aug 20 13:41:53 2015 +0200
@@ -11,7 +11,7 @@
val add: string -> T -> T
val markup: Markup.T -> (T -> T) -> T -> T
val content: T -> string
- val output: T -> TextIO.outstream -> unit
+ val output: T -> BinIO.outstream -> unit
end;
structure Buffer: BUFFER =
@@ -29,6 +29,8 @@
in add bg #> body #> add en end;
fun content (Buffer xs) = implode (rev xs);
-fun output (Buffer xs) stream = List.app (fn s => TextIO.output (stream, s)) (rev xs);
+
+fun output (Buffer xs) stream =
+ List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (rev xs);
end;
--- a/src/Pure/General/file.ML Wed Aug 19 22:40:41 2015 +0200
+++ b/src/Pure/General/file.ML Thu Aug 20 13:41:53 2015 +0200
@@ -20,9 +20,9 @@
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: (TextIO.instream -> 'a) -> Path.T -> 'a
- val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
- val open_append: (TextIO.outstream -> '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 fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
@@ -32,6 +32,7 @@
val read: Path.T -> string
val write: Path.T -> string -> unit
val append: Path.T -> string -> unit
+ val output: BinIO.outstream -> string -> 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
@@ -104,9 +105,9 @@
in
fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
-fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path;
-fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path;
-fun open_append f = with_file TextIO.openAppend TextIO.closeOut 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;
@@ -134,7 +135,7 @@
fun fold_chunks terminator f path a = open_input (fn file =>
let
fun read buf x =
- (case TextIO.input file of
+ (case Byte.bytesToString (BinIO.input file) of
"" => (case Buffer.content buf of "" => x | line => f line x)
| input =>
(case String.fields (fn c => c = terminator) input of
@@ -150,15 +151,16 @@
fun read_lines path = rev (fold_lines cons path []);
fun read_pages path = rev (fold_pages cons path []);
-val read = open_input TextIO.inputAll;
+val read = open_input (Byte.bytesToString o BinIO.inputAll);
(* output *)
-fun output txts file = List.app (fn txt => TextIO.output (file, txt)) txts;
+fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
-fun write_list path txts = open_output (output txts) path;
-fun append_list path txts = open_append (output txts) path;
+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 path txt = write_list path [txt];
fun append path txt = append_list path [txt];
--- a/src/Pure/PIDE/xml.ML Wed Aug 19 22:40:41 2015 +0200
+++ b/src/Pure/PIDE/xml.ML Thu Aug 20 13:41:53 2015 +0200
@@ -44,7 +44,7 @@
val output_markup: Markup.T -> Output.output * Output.output
val string_of: tree -> string
val pretty: int -> tree -> Pretty.T
- val output: tree -> TextIO.outstream -> unit
+ val output: tree -> BinIO.outstream -> unit
val parse_comments: string list -> unit * string list
val parse_string : string -> string option
val parse_element: string list -> tree * string list
--- a/src/Pure/System/system_channel.ML Wed Aug 19 22:40:41 2015 +0200
+++ b/src/Pure/System/system_channel.ML Thu Aug 20 13:41:53 2015 +0200
@@ -36,7 +36,7 @@
else Byte.bytesToString (BinIO.inputN (in_stream, n));
fun output (System_Channel (_, out_stream)) s =
- BinIO.output (out_stream, Byte.stringToBytes s);
+ File.output out_stream s;
fun flush (System_Channel (_, out_stream)) =
BinIO.flushOut out_stream;
@@ -48,4 +48,3 @@
in System_Channel (in_stream, out_stream) end;
end;
-