# HG changeset patch # User wenzelm # Date 1544632469 -3600 # Node ID ef051edd4d10b2cd971e8eac0a856859a9b47714 # Parent dcea1fffbfe6e3597522364f14f9c096cfa02e37 more uniform multi-language operations; misc tuning and clarification; diff -r dcea1fffbfe6 -r ef051edd4d10 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Wed Dec 12 14:19:56 2018 +0100 +++ b/src/Pure/General/bytes.scala Wed Dec 12 17:34:29 2018 +0100 @@ -39,6 +39,7 @@ new Bytes(b, 0, b.length) } + val newline: Bytes = apply("\n") def base64(s: String): Bytes = { diff -r dcea1fffbfe6 -r ef051edd4d10 src/Pure/PIDE/byte_message.ML --- a/src/Pure/PIDE/byte_message.ML Wed Dec 12 14:19:56 2018 +0100 +++ b/src/Pure/PIDE/byte_message.ML Wed Dec 12 17:34:29 2018 +0100 @@ -6,20 +6,13 @@ signature BYTE_MESSAGE = sig - val write: BinIO.outstream -> string -> unit + val write: BinIO.outstream -> string list -> unit val flush: BinIO.outstream -> unit - val read: BinIO.instream -> int -> string val read_block: BinIO.instream -> int -> string option * int val read_line: BinIO.instream -> string option - - val write_header: BinIO.outstream -> int list -> unit - val read_header: BinIO.instream -> int list option - val read_header1: BinIO.instream -> int option - val write_message: BinIO.outstream -> string list -> unit val read_message: BinIO.instream -> string list option - val write_line_message: BinIO.outstream -> string -> unit val read_line_message: BinIO.instream -> string option end; @@ -29,9 +22,7 @@ (* output operations *) -fun write stream s = BinIO.output (stream, Byte.stringToBytes s); - -fun newline stream = write stream "\n"; +fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)); fun flush stream = ignore (try BinIO.flushOut stream); @@ -59,35 +50,17 @@ in read_body [] end; -(* header with chunk lengths *) +(* messages with multiple chunks (arbitrary content) *) -fun write_header stream ns = - (write stream (space_implode "," (map string_of_int ns)); - newline stream); +fun make_header stream ns = + [space_implode "," (map Value.print_int ns), "\n"]; -fun err_header line = - error ("Malformed message header: " ^ quote line); +fun write_message stream chunks = + (write stream (make_header stream (map size chunks) @ chunks); flush stream); fun parse_header line = map Value.parse_nat (space_explode "," line) - handle Fail _ => err_header line - -fun read_header stream = - read_line stream |> Option.map parse_header; - -fun read_header1 stream = - read_line stream |> Option.map (fn line => - (case parse_header line of - [n] => n - | _ => err_header line)); - - -(* messages with multiple chunks (arbitrary content) *) - -fun write_message stream chunks = - (write_header stream (map size chunks); - List.app (write stream) chunks; - flush stream); + handle Fail _ => error ("Malformed message header: " ^ quote line); fun read_chunk stream n = (case read_block stream n of @@ -97,7 +70,7 @@ string_of_int len ^ " of " ^ string_of_int n ^ " bytes")); fun read_message stream = - read_header stream |> (Option.map o map) (read_chunk stream); + read_line stream |> Option.map (parse_header #> map (read_chunk stream)); (* hybrid messages: line or length+block (with content restriction) *) @@ -114,10 +87,9 @@ 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] - else (); - write stream msg; - newline stream; + write stream + ((if n > 100 orelse exists_string (fn s => s = "\n") msg + then make_header stream [n + 1] else []) @ [msg, "\n"]); flush stream end; diff -r dcea1fffbfe6 -r ef051edd4d10 src/Pure/PIDE/byte_message.scala --- a/src/Pure/PIDE/byte_message.scala Wed Dec 12 14:19:56 2018 +0100 +++ b/src/Pure/PIDE/byte_message.scala Wed Dec 12 17:34:29 2018 +0100 @@ -13,9 +13,8 @@ { /* output operations */ - def write(stream: OutputStream, bytes: Bytes) { bytes.write_stream(stream) } - - def newline(stream: OutputStream) { stream.write(10) } + def write(stream: OutputStream, bytes: List[Bytes]): Unit = + bytes.foreach(_.write_stream(stream)) def flush(stream: OutputStream): Unit = try { stream.flush() } @@ -50,40 +49,20 @@ } - /* header with chunk lengths */ + /* messages with multiple chunks (arbitrary content) */ - def write_header(stream: OutputStream, ns: List[Int]) + private def make_header(ns: List[Int]): List[Bytes] = + List(Bytes(ns.mkString(",")), Bytes.newline) + + def write_message(stream: OutputStream, chunks: List[Bytes]) { - stream.write(UTF8.bytes(ns.mkString(","))) - newline(stream) + write(stream, make_header(chunks.map(_.length)) ::: chunks) + flush(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.Nat.parse) } - catch { case ERROR(_) => err_header(line) } - - def read_header(stream: InputStream): Option[List[Int]] = - read_line(stream).map(_.text).map(parse_header(_)) - - def read_header1(stream: InputStream): Option[Int] = - read_line(stream).map(_.text).map(line => - parse_header(line) match { - case List(n) => n - case _ => err_header(line) - }) - - - /* messages with multiple chunks (arbitrary content) */ - - def write_message(stream: OutputStream, chunks: List[Bytes]) - { - write_header(stream, chunks.map(_.length)) - chunks.foreach(write(stream, _)) - flush(stream) - } + catch { case ERROR(_) => error("Malformed message header: " + quote(line)) } private def read_chunk(stream: InputStream, n: Int): Bytes = read_block(stream, n) match { @@ -93,7 +72,7 @@ } def read_message(stream: InputStream): Option[List[Bytes]] = - read_header(stream).map(ns => ns.map(n => read_chunk(stream, n))) + read_line(stream).map(line => parse_header(line.text).map(read_chunk(stream, _))) /* hybrid messages: line or length+block (restricted content) */ @@ -113,10 +92,9 @@ error ("Bad content for line message:\n" ++ msg.text.take(100)) val n = msg.length - if (n > 100 || msg.iterator.contains(10)) write_header(stream, List(n + 1)) - - write(stream, msg) - newline(stream) + write(stream, + (if (n > 100 || msg.iterator.contains(10)) make_header(List(n + 1)) else Nil) ::: + List(msg, Bytes.newline)) flush(stream) } diff -r dcea1fffbfe6 -r ef051edd4d10 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Wed Dec 12 14:19:56 2018 +0100 +++ b/src/Tools/Haskell/Haskell.thy Wed Dec 12 17:34:29 2018 +0100 @@ -1409,13 +1409,14 @@ -} module Isabelle.Byte_Message ( - write, newline, - read, read_block, trim_line, read_line, - read_line_message, write_line_message + write, read, read_block, trim_line, read_line, + write_message, read_message, + write_line_message, read_line_message ) where import Prelude hiding (read) +import Data.Maybe import Data.ByteString (ByteString) import qualified Data.ByteString as ByteString import qualified Data.ByteString.UTF8 as UTF8 @@ -1426,6 +1427,7 @@ import qualified Network.Socket as Socket import qualified Network.Socket.ByteString as ByteString +import Isabelle.Library hiding (trim_line) import qualified Isabelle.Value as Value @@ -1482,6 +1484,42 @@ b -> read_body (b : bs) +{- messages with multiple chunks (arbitrary content) -} + +make_header :: [Int] -> [ByteString] +make_header ns = + [UTF8.fromString (space_implode "," (map Value.print_int ns)), newline] + +write_message :: Socket -> [ByteString] -> IO () +write_message socket chunks = + write socket (make_header (map ByteString.length chunks) ++ chunks) + +parse_header :: ByteString -> [Int] +parse_header line = + let + res = map Value.parse_nat (space_explode ',' (UTF8.toString line)) + in + if all isJust res then map fromJust res + else error ("Malformed message header: " ++ quote (UTF8.toString line)) + +read_chunk :: Socket -> Int -> IO ByteString +read_chunk socket n = do + res <- read_block socket n + return $ + case res of + (Just chunk, _) -> chunk + (Nothing, len) -> + error ("Malformed message chunk: unexpected EOF after " ++ + show len ++ " of " ++ show n ++ " bytes") + +read_message :: Socket -> IO (Maybe [ByteString]) +read_message socket = do + res <- read_line socket + case res of + Just line -> Just <$> mapM (read_chunk socket) (parse_header line) + Nothing -> return Nothing + + -- hybrid messages: line or length+block (with content restriction) is_length :: ByteString -> Bool @@ -1498,10 +1536,9 @@ error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg)) let n = ByteString.length msg - write socket - (if n > 100 || ByteString.any (== 10) msg then - [UTF8.fromString (Value.print_int (n + 1)), newline, msg, newline] - else [msg, newline]) + write socket $ + (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) ++ + [msg, newline] read_line_message :: Socket -> IO (Maybe ByteString) read_line_message socket = do