# HG changeset patch # User wenzelm # Date 1544644310 -3600 # Node ID 7258ebf38662649c60926e8e49db4cb762fc8e45 # Parent 6a901078a294758f0a8b1e13a12aace1f082b962# Parent b7b9cbe0bd432c6a41b1c3ee6afce00e5a533324 merged; diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/General/bytes.scala Wed Dec 12 20:51:50 2018 +0100 @@ -39,6 +39,7 @@ new Bytes(b, 0, b.length) } + val newline: Bytes = apply("\n") def base64(s: String): Bytes = { @@ -64,27 +65,6 @@ 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)) @@ -136,6 +116,12 @@ lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes) + def is_empty: Boolean = length == 0 + + def iterator: Iterator[Byte] = + for (i <- (offset until (offset + length)).iterator) + yield bytes(i) + def array: Array[Byte] = { val a = new Array[Byte](length) @@ -190,6 +176,13 @@ else throw new IndexOutOfBoundsException } + def trim_line: Bytes = + if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10) + subSequence(0, length - 2) + else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10)) + subSequence(0, length - 1) + else this + /* streams */ diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/General/symbol.ML Wed Dec 12 20:51:50 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; diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/General/symbol.scala Wed Dec 12 20:51:50 2018 +0100 @@ -48,6 +48,8 @@ def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c) + def is_ascii_line_terminator(c: Char): Boolean = "\r\n".contains(c) + def is_ascii_letdig(c: Char): Boolean = is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c) diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/General/value.scala --- a/src/Pure/General/value.scala Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/General/value.scala Wed Dec 12 20:51:50 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) diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/PIDE/byte_message.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/byte_message.ML Wed Dec 12 20:51:50 2018 +0100 @@ -0,0 +1,104 @@ +(* Title: Pure/General/byte_message.ML + Author: Makarius + +Byte-oriented messages. +*) + +signature BYTE_MESSAGE = +sig + 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_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; + +structure Byte_Message: BYTE_MESSAGE = +struct + +(* output operations *) + +fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)); + +fun flush stream = ignore (try BinIO.flushOut stream); + + +(* input operations *) + +fun read stream n = Byte.bytesToString (BinIO.inputN (stream, n)); + +fun read_block stream n = + 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_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_body (c :: cs))); + in read_body [] end; + + +(* messages with multiple chunks (arbitrary content) *) + +fun make_header stream ns = + [space_implode "," (map Value.print_int ns), "\n"]; + +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 _ => error ("Malformed message header: " ^ quote line); + +fun read_chunk stream n = + (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")); + +fun read_message stream = + read_line stream |> Option.map (parse_header #> map (read_chunk stream)); + + +(* hybrid messages: line or length+block (with content restriction) *) + +fun is_length msg = + msg <> "" andalso forall_string Symbol.is_ascii_digit msg; + +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 is_terminated msg then + error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg))) + else + let val n = size msg in + 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; + +fun read_line_message stream = + (case read_line stream of + NONE => NONE + | SOME line => + (case try Value.parse_nat line of + NONE => SOME line + | SOME n => Option.map trim_line (#1 (read_block stream n)))); + +end; diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/PIDE/byte_message.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/byte_message.scala Wed Dec 12 20:51:50 2018 +0100 @@ -0,0 +1,110 @@ +/* Title: Pure/General/byte_message.scala + Author: Makarius + +Byte-oriented messages. +*/ + +package isabelle + +import java.io.{ByteArrayOutputStream, OutputStream, InputStream, IOException} + + +object Byte_Message +{ + /* output operations */ + + def write(stream: OutputStream, bytes: List[Bytes]): Unit = + bytes.foreach(_.write_stream(stream)) + + def flush(stream: OutputStream): Unit = + try { stream.flush() } + catch { case _: IOException => } + + + /* input operations */ + + def read(stream: InputStream, n: Int): Bytes = + Bytes.read_stream(stream, limit = n) + + def read_block(stream: InputStream, n: Int): (Option[Bytes], Int) = + { + val msg = read(stream, n) + val len = msg.length + (if (len == n) Some(msg) else None, len) + } + + def read_line(stream: InputStream): Option[Bytes] = + { + val line = new ByteArrayOutputStream(100) + var c = 0 + while ({ c = stream.read; c != -1 && c != 10 }) line.write(c) + + if (c == -1 && line.size == 0) None + else { + val a = line.toByteArray + val n = a.length + val len = if (n > 0 && a(n - 1) == 13) n - 1 else n + Some(Bytes(a, 0, len)) + } + } + + + /* messages with multiple chunks (arbitrary content) */ + + private def make_header(ns: List[Int]): List[Bytes] = + List(Bytes(ns.mkString(",")), Bytes.newline) + + def write_message(stream: OutputStream, chunks: List[Bytes]) + { + write(stream, make_header(chunks.map(_.length)) ::: chunks) + flush(stream) + } + + private def parse_header(line: String): List[Int] = + try { space_explode(',', line).map(Value.Nat.parse) } + catch { case ERROR(_) => error("Malformed message header: " + quote(line)) } + + private def read_chunk(stream: InputStream, n: Int): 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_line(stream).map(line => parse_header(line.text).map(read_chunk(stream, _))) + + + /* hybrid messages: line or length+block (restricted content) */ + + private def is_length(msg: Bytes): Boolean = + !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) + + private def is_terminated(msg: Bytes): Boolean = + { + val len = msg.length + len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1)) + } + + def write_line_message(stream: OutputStream, msg: Bytes) + { + if (is_length(msg) || is_terminated(msg)) + error ("Bad content for line message:\n" ++ msg.text.take(100)) + + val n = msg.length + write(stream, + (if (n > 100 || msg.iterator.contains(10)) make_header(List(n + 1)) else Nil) ::: + List(msg, Bytes.newline)) + flush(stream) + } + + def read_line_message(stream: InputStream): Option[Bytes] = + read_line(stream) match { + case None => None + case Some(line) => + Value.Nat.unapply(line.text) match { + case None => Some(line) + case Some(n) => read_block(stream, n)._1.map(_.trim_line) + } + } +} diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/ROOT.ML Wed Dec 12 20:51:50 2018 +0100 @@ -83,12 +83,12 @@ 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"; ML_file "General/sha1.ML"; +ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/document_id.ML"; @@ -318,7 +318,6 @@ subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; -ML_file "System/system_channel.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/invoke_scala.ML"; diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/System/isabelle_process.ML Wed Dec 12 20:51:50 2018 +0100 @@ -95,12 +95,13 @@ val serial_props = Markup.serial_properties o serial; -fun init_channels channel = +fun init_channels out_stream = let val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); + val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); - val msg_channel = Message_Channel.make channel; + val msg_channel = Message_Channel.make out_stream; fun message name props body = Message_Channel.send msg_channel (Message_Channel.message name props body); @@ -149,37 +150,18 @@ Output.physical_stderr "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); -fun read_chunk channel len = - let - val n = - (case Int.fromString len of - SOME n => n - | NONE => error ("Isabelle process: malformed header " ^ quote len)); - val chunk = System_Channel.inputN channel n; - val i = size chunk; - in - if i <> n then - error ("Isabelle process: bad chunk (unexpected EOF after " ^ - string_of_int i ^ " of " ^ string_of_int n ^ " bytes)") - else chunk - end; - -fun read_command channel = - System_Channel.input_line channel - |> Option.map (fn line => map (read_chunk channel) (space_explode "," line)); - in -fun loop channel = +fun loop stream = let val continue = - (case read_command channel of + (case Byte_Message.read_message stream of NONE => false | SOME [] => (Output.system_message "Isabelle process: no input"; true) | SOME (name :: args) => (run_command name args; true)) handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true); in - if continue then loop channel + if continue then loop stream else (Future.shutdown (); Execution.reset (); ()) end; @@ -202,9 +184,9 @@ Unsynchronized.change print_mode (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); - val channel = System_Channel.rendezvous socket; - val msg_channel = init_channels channel; - val _ = loop channel; + val (in_stream, out_stream) = Socket_IO.open_streams socket; + val msg_channel = init_channels out_stream; + val _ = loop in_stream; val _ = Message_Channel.shutdown msg_channel; val _ = Private_Output.init_channels (); diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/System/message_channel.ML Wed Dec 12 20:51:50 2018 +0100 @@ -11,7 +11,7 @@ type T val send: T -> message -> unit val shutdown: T -> unit - val make: System_Channel.T -> T + val make: BinIO.outstream -> T end; structure Message_Channel: MESSAGE_CHANNEL = @@ -30,8 +30,8 @@ val header = YXML.string_of (XML.Elem ((name, robust_props), [])); in Message (chunk [header] @ chunk body) end; -fun output_message channel (Message ss) = - List.app (System_Channel.output channel) ss; +fun output_message stream (Message ss) = + List.app (File.output stream) ss; (* channel *) @@ -41,26 +41,25 @@ fun send (Message_Channel {send, ...}) = send; fun shutdown (Message_Channel {shutdown, ...}) = shutdown (); -fun flush channel = ignore (try System_Channel.flush channel); val flush_timeout = SOME (seconds 0.02); -fun message_output mbox channel = +fun message_output mbox stream = let fun continue timeout = (case Mailbox.receive timeout mbox of - [] => (flush channel; continue NONE) + [] => (Byte_Message.flush stream; continue NONE) | msgs => received timeout msgs) - and received _ (NONE :: _) = flush channel - | received _ (SOME msg :: rest) = (output_message channel msg; received flush_timeout rest) + and received _ (NONE :: _) = Byte_Message.flush stream + | received _ (SOME msg :: rest) = (output_message stream msg; received flush_timeout rest) | received timeout [] = continue timeout; in fn () => continue NONE end; -fun make channel = +fun make stream = let val mbox = Mailbox.create (); val thread = Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false} - (message_output mbox channel); + (message_output mbox stream); fun send msg = Mailbox.send mbox (SOME msg); fun shutdown () = (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread); diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/System/system_channel.ML --- a/src/Pure/System/system_channel.ML Wed Dec 12 13:32:06 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -(* Title: Pure/System/system_channel.ML - Author: Makarius - -Socket-based system channel for inter-process communication. -*) - -signature SYSTEM_CHANNEL = -sig - type T - val input_line: T -> string option - val inputN: T -> int -> string - val output: T -> string -> unit - val flush: T -> unit - val rendezvous: string -> T -end; - -structure System_Channel: SYSTEM_CHANNEL = -struct - -datatype T = System_Channel of BinIO.instream * BinIO.outstream; - -fun input_line (System_Channel (stream, _)) = Bytes.read_line stream; -fun inputN (System_Channel (stream, _)) n = Bytes.read_block stream n; - -fun output (System_Channel (_, stream)) s = File.output stream s; -fun flush (System_Channel (_, stream)) = BinIO.flushOut stream; - -fun rendezvous name = - let - val (in_stream, out_stream) = Socket_IO.open_streams name; - val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); - in System_Channel (in_stream, out_stream) end; - -end; diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/Tools/server.scala Wed Dec 12 20:51:50 2018 +0100 @@ -181,26 +181,11 @@ interrupt = interrupt) def read_message(): Option[String] = - try { - Bytes.read_line(in).map(_.text) match { - case Some(Value.Int(n)) => - Bytes.read_block(in, n).map(bytes => Library.trim_line(bytes.text)) - case res => res - } - } - catch { case _: SocketException => None } + try { Byte_Message.read_line_message(in).map(_.text) } + catch { case _: IOException => None } - def write_message(msg: String): Unit = out_lock.synchronized - { - val b = UTF8.bytes(msg) - if (b.length > 100 || b.contains(10)) { - out.write(UTF8.bytes((b.length + 1).toString)) - out.write(10) - } - out.write(b) - out.write(10) - try { out.flush() } catch { case _: SocketException => } - } + def write_message(msg: String): Unit = + out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) } def reply(r: Reply.Value, arg: Any) { diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Pure/build-jars --- a/src/Pure/build-jars Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Pure/build-jars Wed Dec 12 20:51:50 2018 +0100 @@ -89,6 +89,7 @@ ML/ml_process.scala ML/ml_statistics.scala ML/ml_syntax.scala + PIDE/byte_message.scala PIDE/command.scala PIDE/command_span.scala PIDE/document.scala diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Tools/Haskell/Haskell.thy Wed Dec 12 20:51:50 2018 +0100 @@ -25,10 +25,13 @@ fold, fold_rev, single, map_index, get_index, - quote, trim_line, clean_name) + quote, space_implode, commas, commas_quote, cat_lines, + space_explode, split_lines, trim_line, clean_name) where import Data.Maybe +import qualified Data.List as List +import qualified Data.List.Split as Split {- functions -} @@ -91,6 +94,23 @@ quote :: String -> String quote s = "\"" ++ s ++ "\"" +space_implode :: String -> [String] -> String +space_implode = List.intercalate + +commas, commas_quote :: [String] -> String +commas = space_implode ", " +commas_quote = commas . map quote + +cat_lines :: [String] -> String +cat_lines = space_implode "\n" + + +space_explode :: Char -> String -> [String] +space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c))) + +split_lines :: String -> [String] +split_lines = space_explode '\n' + trim_line :: String -> String trim_line line = case reverse line of @@ -113,7 +133,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 +153,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 @@ -1103,7 +1132,7 @@ commas, enclose, enum, list, str_list, big_list) where -import Isabelle.Library hiding (quote) +import Isabelle.Library hiding (quote, commas) import qualified Data.List as List import qualified Isabelle.Buffer as Buffer import qualified Isabelle.Markup as Markup @@ -1368,86 +1397,201 @@ \([], a) -> App (pair term term a)] \ -generate_file "Isabelle/Bytes.hs" = \ -{- Title: Isabelle/Bytes.hs +generate_file "Isabelle/Byte_Message.hs" = \ +{- Title: Isabelle/Byte_Message.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) -Byte-vector messages. +Byte-oriented messages. + +See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\ +and \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\. -} -module Isabelle.Bytes (read_line, read_block, read_message, write_message) +module Isabelle.Byte_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 import Data.Word (Word8) +import Control.Monad (when) import Network.Socket (Socket) 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 --- see also \<^file>\$ISABELLE_HOME/src/Pure/General/bytes.ML\ +{- 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_body 0 [] + where + result = ByteString.concat . reverse + 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_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) + +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) - -read_block :: Socket -> Int -> IO ByteString -read_block socket n = read 0 [] - where - result :: [ByteString] -> ByteString - result = ByteString.concat . reverse - - read :: Int -> [ByteString] -> IO ByteString - read 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 (len + m) (s : ss)) + b -> read_body (b : bs) --- see also \<^file>\$ISABELLE_HOME/src/Pure/Tools/server.scala\ +{- 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 -> 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 +is_length msg = + not (ByteString.null msg) && ByteString.all (\b -> 48 <= b && b <= 57) msg + +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 || is_terminated msg) $ + 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 make_header [n + 1] else []) ++ + [msg, newline] + +read_line_message :: Socket -> IO (Maybe ByteString) +read_line_message socket = do opt_line <- read_line socket 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 -> Just <$> read_block socket n + Just n -> fmap trim_line . fst <$> read_block socket n +\ + +generate_file "Isabelle/Server.hs" = \ +{- Title: Isabelle/Server.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +TCP server on localhost. +-} + +module Isabelle.Server (server) where + +import Control.Monad (forever) +import qualified Control.Exception as Exception +import Network.Socket (Socket) +import qualified Network.Socket as Socket +import qualified Control.Concurrent as Concurrent + -write_message :: Socket -> ByteString -> IO () -write_message socket msg = do - let newline = ByteString.singleton 10 - let n = ByteString.length msg - ByteString.sendMany socket - (if n > 100 || ByteString.any (== 10) msg then - [UTF8.fromString (Value.print_int (n + 1)), newline, msg, newline] - else [msg, newline]) +localhost :: Socket.HostAddress +localhost = Socket.tupleToHostAddress (127, 0, 0, 1) + +localhost_name :: String +localhost_name = "127.0.0.1" + +server :: (String -> IO ()) -> (Socket -> IO ()) -> IO () +server publish handle = + Socket.withSocketsDo $ Exception.bracket open Socket.close loop + where + open :: IO Socket + open = do + socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol + Socket.bind socket (Socket.SockAddrInet 0 localhost) + Socket.listen socket 50 + port <- Socket.socketPort socket + publish (localhost_name ++ ":" ++ show port) + return socket + + loop :: Socket -> IO () + loop socket = forever $ do + (connection, peer) <- Socket.accept socket + Concurrent.forkFinally (handle connection) (\_ -> Socket.close connection) + return () \ end diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Tools/Haskell/Test.thy --- a/src/Tools/Haskell/Test.thy Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Tools/Haskell/Test.thy Wed Dec 12 20:51:50 2018 +0100 @@ -17,7 +17,9 @@ |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode "."); val _ = GHC.new_project tmp_dir - {name = "isabelle", depends = ["bytestring", "utf8-string", "network"], modules = modules}; + {name = "isabelle", + depends = ["bytestring", "network", "split", "utf8-string"], + modules = modules}; val (out, rc) = Isabelle_System.bash_output diff -r b7b9cbe0bd43 -r 7258ebf38662 src/Tools/VSCode/src/channel.scala --- a/src/Tools/VSCode/src/channel.scala Wed Dec 12 13:32:06 2018 +0100 +++ b/src/Tools/VSCode/src/channel.scala Wed Dec 12 20:51:50 2018 +0100 @@ -21,7 +21,7 @@ private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r private def read_line(): String = - Bytes.read_line(in) match { + Byte_Message.read_line(in) match { case Some(bytes) => bytes.text case None => "" }