--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/bytes.ML Mon Dec 10 20:20:24 2018 +0100
@@ -0,0 +1,31 @@
+(* Title: Pure/General/bytes.ML
+ Author: Makarius
+
+Immutable byte vectors as ML strings.
+*)
+
+signature BYTES =
+sig
+ val read_line: BinIO.instream -> string option
+ val read_block: BinIO.instream -> int -> string
+end;
+
+structure Bytes: BYTES =
+struct
+
+fun read_line stream =
+ let
+ val result = trim_line o String.implode o rev;
+ fun read cs =
+ (case BinIO.input1 stream of
+ NONE => if null cs then NONE else SOME (result cs)
+ | SOME b =>
+ (case Byte.byteToChar b of
+ #"\n" => SOME (result cs)
+ | c => read (c :: cs)));
+ in read [] end;
+
+fun read_block stream n =
+ Byte.bytesToString (BinIO.inputN (stream, n));
+
+end;
--- a/src/Pure/ROOT.ML Mon Dec 10 20:00:02 2018 +0100
+++ b/src/Pure/ROOT.ML Mon Dec 10 20:20:24 2018 +0100
@@ -83,6 +83,7 @@
ML_file "General/file.ML";
ML_file "General/long_name.ML";
ML_file "General/binding.ML";
+ML_file "General/bytes.ML";
ML_file "General/socket_io.ML";
ML_file "General/seq.ML";
ML_file "General/timing.ML";
--- a/src/Pure/System/system_channel.ML Mon Dec 10 20:00:02 2018 +0100
+++ b/src/Pure/System/system_channel.ML Mon Dec 10 20:20:24 2018 +0100
@@ -19,26 +19,11 @@
datatype T = System_Channel of BinIO.instream * BinIO.outstream;
-fun input_line (System_Channel (in_stream, _)) =
- let
- val result = trim_line o String.implode o rev;
- fun read cs =
- (case BinIO.input1 in_stream of
- NONE => if null cs then NONE else SOME (result cs)
- | SOME b =>
- (case Byte.byteToChar b of
- #"\n" => SOME (result cs)
- | c => read (c :: cs)));
- in read [] end;
+fun input_line (System_Channel (stream, _)) = Bytes.read_line stream;
+fun inputN (System_Channel (stream, _)) n = Bytes.read_block stream n;
-fun inputN (System_Channel (in_stream, _)) n =
- Byte.bytesToString (BinIO.inputN (in_stream, n));
-
-fun output (System_Channel (_, out_stream)) s =
- File.output out_stream s;
-
-fun flush (System_Channel (_, out_stream)) =
- BinIO.flushOut out_stream;
+fun output (System_Channel (_, stream)) s = File.output stream s;
+fun flush (System_Channel (_, stream)) = BinIO.flushOut stream;
fun rendezvous name =
let