# HG changeset patch # User wenzelm # Date 1544614265 -3600 # Node ID 704915cf59fa6acb3647729d328c5c09abe3242d # Parent 387894c2fb2c21738e771d94cf9cdf384d3ee9f8 more uniform multi-language operations; misc tuning and clarification; diff -r 387894c2fb2c -r 704915cf59fa src/Pure/General/symbol.ML --- 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; diff -r 387894c2fb2c -r 704915cf59fa src/Pure/General/value.scala --- 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 diff -r 387894c2fb2c -r 704915cf59fa src/Pure/PIDE/byte_message.ML --- 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; diff -r 387894c2fb2c -r 704915cf59fa src/Pure/PIDE/byte_message.scala --- 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) + } } } diff -r 387894c2fb2c -r 704915cf59fa src/Tools/Haskell/Haskell.thy --- 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>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\. -} -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 \ end