# HG changeset patch
# User wenzelm
# Date 1544469624 -3600
# Node ID 0bd51c6aaa8b1cd614fbcf372afe564fa0e63bba
# Parent  eaf66384cfe852e199ca847c8b16647230b8ff7e
clarified modules, following bytes.scala;

diff -r eaf66384cfe8 -r 0bd51c6aaa8b src/Pure/General/bytes.ML
--- /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;
diff -r eaf66384cfe8 -r 0bd51c6aaa8b src/Pure/ROOT.ML
--- 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";
diff -r eaf66384cfe8 -r 0bd51c6aaa8b src/Pure/System/system_channel.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