# HG changeset patch
# User wenzelm
# Date 1440070913 -7200
# Node ID 67e389f67073e8c9c59bd1f46c9e65529587ca91
# Parent  e1159bd15982c62d94073bba445c23d3ead3bd44
precise BinIO, without newline conversion on Windows;

diff -r e1159bd15982 -r 67e389f67073 src/HOL/TPTP/TPTP_Parser/tptp_parser.ML
--- 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
diff -r e1159bd15982 -r 67e389f67073 src/HOL/Tools/sat_solver.ML
--- 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
diff -r e1159bd15982 -r 67e389f67073 src/Pure/General/buffer.ML
--- 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;
diff -r e1159bd15982 -r 67e389f67073 src/Pure/General/file.ML
--- 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];
diff -r e1159bd15982 -r 67e389f67073 src/Pure/PIDE/xml.ML
--- 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
diff -r e1159bd15982 -r 67e389f67073 src/Pure/System/system_channel.ML
--- 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;
-