--- 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 */
--- 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;
--- 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)
--- 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)
--- /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;
--- /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)
+ }
+ }
+}
--- 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";
--- 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 ();
--- 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);
--- 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;
--- 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)
{
--- 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
--- 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)]
\<close>
-generate_file "Isabelle/Bytes.hs" = \<open>
-{- Title: Isabelle/Bytes.hs
+generate_file "Isabelle/Byte_Message.hs" = \<open>
+{- Title: Isabelle/Byte_Message.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
-Byte-vector messages.
+Byte-oriented messages.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
-}
-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>\<open>$ISABELLE_HOME/src/Pure/General/bytes.ML\<close>
+{- 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>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close>
+{- 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
+\<close>
+
+generate_file "Isabelle/Server.hs" = \<open>
+{- 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 ()
\<close>
end
--- 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
--- 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 => ""
}