# HG changeset patch
# User wenzelm
# Date 1520679354 -3600
# Node ID 2d9a265b294ec1e2756d64187a32876ef1c4019b
# Parent  c67fb01921ebaecbc8e9d16f934bfcddc2b829a3
more uniform Bytes.read_line/read_block operations;

diff -r c67fb01921eb -r 2d9a265b294e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Mar 10 11:40:25 2018 +0100
+++ b/src/Pure/General/bytes.scala	Sat Mar 10 11:55:54 2018 +0100
@@ -56,6 +56,27 @@
       new Bytes(out.toByteArray, 0, out.size)
     }
 
+  def read_block(stream: InputStream, length: Int): Option[Bytes] =
+  {
+    val bytes = read_stream(stream, limit = length)
+    if (bytes.length == length) Some(bytes) else None
+  }
+
+  def read_line(stream: InputStream): Option[Bytes] =
+  {
+    val out = new ByteArrayOutputStream(100)
+    var c = 0
+    while ({ c = stream.read; c != -1 && c != 10 }) out.write(c)
+
+    if (c == -1 && out.size == 0) None
+    else {
+      val a = out.toByteArray
+      val n = a.length
+      val b = if (n > 0 && a(n - 1) == 13) a.take(n - 1) else a
+      Some(new Bytes(b, 0, b.length))
+    }
+  }
+
   def read(file: JFile): Bytes =
     using(new FileInputStream(file))(read_stream(_, file.length.toInt))
 
diff -r c67fb01921eb -r 2d9a265b294e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Mar 10 11:40:25 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sat Mar 10 11:55:54 2018 +0100
@@ -7,8 +7,7 @@
 package isabelle
 
 
-import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
-  IOException}
+import java.io.{BufferedInputStream, BufferedOutputStream, IOException}
 import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
 
 
@@ -62,23 +61,19 @@
 
     def close() { socket.close }
 
-    val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
-    val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
+    val in = new BufferedInputStream(socket.getInputStream)
+    val out = new BufferedOutputStream(socket.getOutputStream)
 
     def read_line(): Option[String] =
-      Exn.capture { reader.readLine() } match {
-        case Exn.Res(null) => None
-        case Exn.Res(line) => Some(line)
-        case Exn.Exn(_: SocketException) => None
-        case Exn.Exn(exn) => throw exn
-      }
+      try { Bytes.read_line(in).map(_.text) }
+      catch { case _: SocketException => None }
 
     def write_line(msg: String)
     {
       require(split_lines(msg).length <= 1)
-      writer.write(msg)
-      writer.newLine()
-      try { writer.flush() } catch { case _: SocketException => }
+      out.write(UTF8.bytes(msg))
+      out.write(10)
+      try { out.flush() } catch { case _: SocketException => }
     }
 
     def reply(r: Server.Reply.Value, t: JSON.T)
diff -r c67fb01921eb -r 2d9a265b294e src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Sat Mar 10 11:40:25 2018 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Sat Mar 10 11:55:54 2018 +0100
@@ -21,12 +21,10 @@
   private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
 
   private def read_line(): String =
-  {
-    val buffer = new ByteArrayOutputStream(100)
-    var c = 0
-    while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
-    Library.trim_line(buffer.toString(UTF8.charset_name))
-  }
+    Bytes.read_line(in) match {
+      case Some(bytes) => bytes.text
+      case None => ""
+    }
 
   private def read_header(): List[String] =
   {
@@ -38,17 +36,9 @@
 
   private def read_content(n: Int): String =
   {
-    val buffer = new Array[Byte](n)
-    var i = 0
-    var m = 0
-    do {
-      m = in.read(buffer, i, n - i)
-      if (m != -1) i += m
-    }
-    while (m != -1 && n > i)
-
-    if (i == n) new String(buffer, UTF8.charset)
-    else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
+    val bytes = Bytes.read_stream(in, limit = n)
+    if (bytes.length == n) bytes.text
+    else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)")
   }
 
   def read(): Option[JSON.T] =