more uniform multi-language operations;
misc tuning and clarification;

--- a/src/Pure/General/symbol.ML	Wed Dec 12 00:01:11 2018 +0100
+++ b/src/Pure/General/symbol.ML	Wed Dec 12 12:31:05 2018 +0100
@@ -36,6 +36,7 @@
   val is_ascii_hex: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
+  val is_ascii_line_terminator: symbol -> bool
   val is_ascii_control: symbol -> bool
   val is_ascii_letdig: symbol -> bool
   val is_ascii_lower: symbol -> bool
@@ -178,6 +179,9 @@
   fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true
     | _ => false;
 
+val is_ascii_line_terminator =
+  fn "\r" => true | "\n" => true | _ => false;
+
 fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
 
 fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;

--- a/src/Pure/General/value.scala	Wed Dec 12 00:01:11 2018 +0100
+++ b/src/Pure/General/value.scala	Wed Dec 12 12:31:05 2018 +0100
@@ -22,6 +22,17 @@
       unapply(s) getOrElse error("Bad boolean: " + quote(s))
   }
 
+  object Nat
+  {
+    def unapply(s: java.lang.String): Option[scala.Int] =
+      s match {
+        case Int(n) if n >= 0 => Some(n)
+        case _ => None
+      }
+    def parse(s: java.lang.String): scala.Int =
+      unapply(s) getOrElse error("Bad natural number: " + quote(s))
+  }
+
   object Int
   {
     def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
@@ -30,12 +41,6 @@
       catch { case _: NumberFormatException => None }
     def parse(s: java.lang.String): scala.Int =
       unapply(s) getOrElse error("Bad integer: " + quote(s))
-
-    def parse_nat(s: java.lang.String): scala.Int =
-      s match {
-        case Value.Int(n) if n >= 0 => n
-        case _ => error("Bad natural number: " + quote(s))
-      }
   }
 
   object Long

--- a/src/Pure/PIDE/byte_message.ML	Wed Dec 12 00:01:11 2018 +0100
+++ b/src/Pure/PIDE/byte_message.ML	Wed Dec 12 12:31:05 2018 +0100
@@ -7,10 +7,10 @@
 signature BYTE_MESSAGE =
 sig
   val write: BinIO.outstream -> string -> unit
-  val newline: BinIO.outstream -> unit
   val flush: BinIO.outstream -> unit
+
   val read: BinIO.instream -> int -> string
-  val read_block: BinIO.instream -> int -> string option
+  val read_block: BinIO.instream -> int -> string option * int
   val read_line: BinIO.instream -> string option
 
   val write_header: BinIO.outstream -> int list -> unit
@@ -41,20 +41,22 @@
 fun read stream n = Byte.bytesToString (BinIO.inputN (stream, n));
 
 fun read_block stream n =
-  let val msg = read stream n
-  in if size msg = n then SOME msg else NONE end;
+  let
+    val msg = read stream n;
+    val len = size msg;
+  in (if len = n then SOME msg else NONE, len) end;
 
 fun read_line stream =
   let
     val result = trim_line o String.implode o rev;
-    fun read cs =
+    fun read_body 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;
+          | c => read_body (c :: cs)));
+  in read_body [] end;
 
 
 (* header with chunk lengths *)
@@ -63,7 +65,8 @@
  (write stream (space_implode "," (map string_of_int ns));
   newline stream);
 
-fun err_header line = error ("Malformed message header: " ^ quote line)
+fun err_header line =
+  error ("Malformed message header: " ^ quote line);
 
 fun parse_header line =
   map Value.parse_nat (space_explode "," line)
@@ -87,15 +90,11 @@
   flush stream);
 
 fun read_chunk stream n =
-  let
-    val chunk = read stream n;
-    val len = size chunk;
-  in
-    if len = n then chunk
-    else
+  (case read_block stream n of
+    (SOME chunk, _) => chunk
+  | (NONE, len) =>
       error ("Malformed message chunk: unexpected EOF after " ^
-        string_of_int len ^ " of " ^ string_of_int n ^ " bytes")
-  end;
+        string_of_int len ^ " of " ^ string_of_int n ^ " bytes"));
 
 fun read_message stream =
   read_header stream |> (Option.map o map) (read_chunk stream);
@@ -103,19 +102,19 @@
 
 (* hybrid messages: line or length+block (with content restriction) *)
 
-fun is_length s =
-  s <> "" andalso forall_string Symbol.is_ascii_digit s;
+fun is_length msg =
+  msg <> "" andalso forall_string Symbol.is_ascii_digit msg;
 
-fun has_line_terminator s =
-  String.isSuffix "\r" s orelse String.isSuffix "\n" s;
+fun is_terminated msg =
+  let val len = size msg
+  in len > 0 andalso Symbol.is_ascii_line_terminator (str (String.sub (msg, len - 1))) end;
 
 fun write_line_message stream msg =
-  if is_length msg orelse has_line_terminator msg then
+  if is_length msg orelse is_terminated msg then
     error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg)))
   else
     let val n = size msg in
-      if n > 100 orelse exists_string (fn s => s = "\n") msg then
-        write_header stream [n + 1]
+      if n > 100 orelse exists_string (fn s => s = "\n") msg then write_header stream [n + 1]
       else ();
       write stream msg;
       newline stream;
@@ -124,10 +123,10 @@
 
 fun read_line_message stream =
   (case read_line stream of
-    SOME line =>
+    NONE => NONE
+  | SOME line =>
       (case try Value.parse_nat line of
         NONE => SOME line
-      | SOME n => Option.map trim_line (read_block stream n))
-  | NONE => NONE) handle IO.Io _ => NONE;
+      | SOME n => Option.map trim_line (#1 (read_block stream n))));
 
 end;

--- a/src/Pure/PIDE/byte_message.scala	Wed Dec 12 00:01:11 2018 +0100
+++ b/src/Pure/PIDE/byte_message.scala	Wed Dec 12 12:31:05 2018 +0100
@@ -24,13 +24,14 @@
 
   /* input operations */
 
-  def read(stream: InputStream, length: Int): Bytes =
-    Bytes.read_stream(stream, limit = length)
+  def read(stream: InputStream, n: Int): Bytes =
+    Bytes.read_stream(stream, limit = n)
 
-  def read_block(stream: InputStream, length: Int): Option[Bytes] =
+  def read_block(stream: InputStream, n: Int): (Option[Bytes], Int) =
   {
-    val msg = read(stream, length)
-    if (msg.length == length) Some(msg) else None
+    val msg = read(stream, n)
+    val len = msg.length
+    (if (len == n) Some(msg) else None, len)
   }
 
   def read_line(stream: InputStream): Option[Bytes] =
@@ -51,11 +52,17 @@
 
   /* header with chunk lengths */
 
+  def write_header(stream: OutputStream, ns: List[Int])
+  {
+    stream.write(UTF8.bytes(ns.mkString(",")))
+    newline(stream)
+  }
+
   private def err_header(line: String): Nothing =
     error("Malformed message header: " + quote(line))
 
   private def parse_header(line: String): List[Int] =
-    try { space_explode(',', line).map(Value.Int.parse_nat) }
+    try { space_explode(',', line).map(Value.Nat.parse) }
     catch { case ERROR(_) => err_header(line) }
 
   def read_header(stream: InputStream): Option[List[Int]] =
@@ -68,12 +75,6 @@
         case _ => err_header(line)
       })
 
-  def write_header(stream: OutputStream, ns: List[Int])
-  {
-    stream.write(UTF8.bytes(ns.mkString(",")))
-    newline(stream)
-  }
-
 
   /* messages with multiple chunks (arbitrary content) */
 
@@ -85,12 +86,11 @@
   }
 
   private def read_chunk(stream: InputStream, n: Int): Bytes =
-  {
-    val chunk = read(stream, n)
-    val len = chunk.length
-    if (len == n) chunk
-    else error("Malformed message chunk: unexpected EOF after " + len + " of " + n + " bytes")
-  }
+    read_block(stream, n) match {
+      case (Some(chunk), _) => chunk
+      case (None, len) =>
+        error("Malformed message chunk: unexpected EOF after " + len + " of " + n + " bytes")
+    }
 
   def read_message(stream: InputStream): Option[List[Bytes]] =
     read_header(stream).map(ns => ns.map(n => read_chunk(stream, n)))
@@ -101,7 +101,7 @@
   private def is_length(msg: Bytes): Boolean =
     !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
 
-  private def has_line_terminator(msg: Bytes): Boolean =
+  private def is_terminated(msg: Bytes): Boolean =
   {
     val len = msg.length
     len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1))
@@ -109,12 +109,12 @@
 
   def write_line_message(stream: OutputStream, msg: Bytes)
   {
-    if (is_length(msg) || has_line_terminator(msg))
+    if (is_length(msg) || is_terminated(msg))
       error ("Bad content for line message:\n" ++ msg.text.take(100))
 
-    if (msg.length > 100 || msg.iterator.contains(10)) {
-      write_header(stream, List(msg.length + 1))
-    }
+    val n = msg.length
+    if (n > 100 || msg.iterator.contains(10)) write_header(stream, List(n + 1))
+
     write(stream, msg)
     newline(stream)
     flush(stream)
@@ -122,9 +122,11 @@
 
   def read_line_message(stream: InputStream): Option[Bytes] =
     read_line(stream) match {
+      case None => None
       case Some(line) =>
-        if (is_length(line)) read_block(stream, Value.Int.parse(line.text)).map(_.trim_line)
-        else Some(line)
-      case None => None
+        Value.Nat.unapply(line.text) match {
+          case None => Some(line)
+          case Some(n) => read_block(stream, n)._1.map(_.trim_line)
+        }
     }
 }

--- a/src/Tools/Haskell/Haskell.thy	Wed Dec 12 00:01:11 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Wed Dec 12 12:31:05 2018 +0100
@@ -113,7 +113,7 @@
 -}
 
 module Isabelle.Value
-  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
+  (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real)
 where
 
 import Data.Maybe
@@ -133,6 +133,15 @@
 parse_bool _ = Nothing
 
 
+{- nat -}
+
+parse_nat :: String -> Maybe Int
+parse_nat s =
+  case Read.readMaybe s of
+    Just n | n >= 0 -> Just n
+    _ -> Nothing
+
+
 {- int -}
 
 print_int :: Int -> String
@@ -1379,9 +1388,11 @@
 and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
 -}
 
-module Isabelle.Byte_Message
-  (read, read_block, read_line, trim_line,
-   read_line_message, write_line_message)
+module Isabelle.Byte_Message (
+    write, newline,
+    read, read_block, trim_line, read_line,
+    read_line_message, write_line_message
+  )
 where
 
 import Prelude hiding (read)
@@ -1398,73 +1409,76 @@
 import qualified Isabelle.Value as Value
 
 
+{- output operations -}
+
+write :: Socket -> [ByteString] -> IO ()
+write = ByteString.sendMany
+
+newline :: ByteString
+newline = ByteString.singleton 10
+
+
+{- input operations -}
+
 read :: Socket -> Int -> IO ByteString
-read socket n = read_bytes 0 []
+read socket n = read_body 0 []
   where
-    result :: [ByteString] -> ByteString
     result = ByteString.concat . reverse
-
-    read_bytes :: Int -> [ByteString] -> IO ByteString
-    read_bytes len ss =
+    read_body len ss =
       if len >= n then return (result ss)
       else
         (do
           s <- ByteString.recv socket (min (n - len) 8192)
           case ByteString.length s of
             0 -> return (result ss)
-            m -> read_bytes (len + m) (s : ss))
+            m -> read_body (len + m) (s : ss))
+
+read_block :: Socket -> Int -> IO (Maybe ByteString, Int)
+read_block socket n = do
+  msg <- read socket n
+  let len = ByteString.length msg
+  return (if len == n then Just msg else Nothing, len)
 
-read_block :: Socket -> Int -> IO (Maybe ByteString)
-read_block socket n = do
-  s <- read socket n
-  return (if ByteString.length s == n then Just s else Nothing)
+trim_line :: ByteString -> ByteString
+trim_line s =
+  if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then ByteString.take (n - 2) s
+  else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then ByteString.take (n - 1) s
+  else s
+  where
+    n = ByteString.length s
+    at = ByteString.index s
 
 read_line :: Socket -> IO (Maybe ByteString)
-read_line socket = read []
+read_line socket = read_body []
   where
-    result :: [Word8] -> ByteString
-    result bs =
-      ByteString.pack $ reverse $
-        if not (null bs) && head bs == 13 then tail bs else bs
-
-    read :: [Word8] -> IO (Maybe ByteString)
-    read bs = do
+    result = trim_line . ByteString.pack . reverse
+    read_body bs = do
       s <- ByteString.recv socket 1
       case ByteString.length s of
         0 -> return (if null bs then Nothing else Just (result bs))
         1 ->
           case ByteString.head s of
             10 -> return (Just (result bs))
-            b -> read (b : bs)
-
-trim_line :: ByteString -> ByteString
-trim_line s =
-    if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then ByteString.take (n - 2) s
-    else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then ByteString.take (n - 1) s
-    else s
-  where
-    n = ByteString.length s
-    at = ByteString.index s
+            b -> read_body (b : bs)
 
 
 -- hybrid messages: line or length+block (with content restriction)
 
 is_length :: ByteString -> Bool
-is_length s =
-  not (ByteString.null s) && ByteString.all (\b -> 48 <= b && b <= 57) s
+is_length msg =
+  not (ByteString.null msg) && ByteString.all (\b -> 48 <= b && b <= 57) msg
 
-has_line_terminator :: ByteString -> Bool
-has_line_terminator s =
-  not (ByteString.null s) && (ByteString.last s == 13 || ByteString.last s == 10)
+is_terminated :: ByteString -> Bool
+is_terminated msg =
+  not (ByteString.null msg) && (ByteString.last msg == 13 || ByteString.last msg == 10)
 
 write_line_message :: Socket -> ByteString -> IO ()
 write_line_message socket msg = do
-  when (is_length msg || has_line_terminator msg) $
+  when (is_length msg || is_terminated msg) $
     error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
 
-  let newline = ByteString.singleton 10
   let n = ByteString.length msg
-  ByteString.sendMany socket
+  write socket
     (if n > 100 || ByteString.any (== 10) msg then
       [UTF8.fromString (Value.print_int (n + 1)), newline, msg, newline]
      else [msg, newline])
@@ -1475,9 +1489,9 @@
   case opt_line of
     Nothing -> return Nothing
     Just line ->
-      case Value.parse_int (UTF8.toString line) of
+      case Value.parse_nat (UTF8.toString line) of
         Nothing -> return $ Just line
-        Just n -> fmap trim_line <$> read_block socket n
+        Just n -> fmap trim_line . fst <$> read_block socket n
 \<close>
 
 end