more uniform multi-language operations;
authorwenzelm
Tue Dec 11 19:25:35 2018 +0100 (19 months ago)
changeset 6944851e696887b81
parent 69446 9cf0b79dfb7f
child 69449 b516fdf8005c
more uniform multi-language operations;
src/Pure/General/bytes.scala
src/Pure/General/symbol.scala
src/Pure/PIDE/byte_message.ML
src/Pure/PIDE/byte_message.scala
src/Pure/ROOT.ML
src/Pure/System/system_channel.ML
src/Pure/Tools/server.scala
src/Pure/build-jars
src/Tools/Haskell/Haskell.thy
src/Tools/VSCode/src/channel.scala
     1.1 --- a/src/Pure/General/bytes.scala	Mon Dec 10 23:36:29 2018 +0100
     1.2 +++ b/src/Pure/General/bytes.scala	Tue Dec 11 19:25:35 2018 +0100
     1.3 @@ -64,27 +64,6 @@
     1.4        new Bytes(out.toByteArray, 0, out.size)
     1.5      }
     1.6  
     1.7 -  def read_block(stream: InputStream, length: Int): Option[Bytes] =
     1.8 -  {
     1.9 -    val bytes = read_stream(stream, limit = length)
    1.10 -    if (bytes.length == length) Some(bytes) else None
    1.11 -  }
    1.12 -
    1.13 -  def read_line(stream: InputStream): Option[Bytes] =
    1.14 -  {
    1.15 -    val out = new ByteArrayOutputStream(100)
    1.16 -    var c = 0
    1.17 -    while ({ c = stream.read; c != -1 && c != 10 }) out.write(c)
    1.18 -
    1.19 -    if (c == -1 && out.size == 0) None
    1.20 -    else {
    1.21 -      val a = out.toByteArray
    1.22 -      val n = a.length
    1.23 -      val b = if (n > 0 && a(n - 1) == 13) a.take(n - 1) else a
    1.24 -      Some(new Bytes(b, 0, b.length))
    1.25 -    }
    1.26 -  }
    1.27 -
    1.28    def read(file: JFile): Bytes =
    1.29      using(new FileInputStream(file))(read_stream(_, file.length.toInt))
    1.30  
    1.31 @@ -136,6 +115,12 @@
    1.32  
    1.33    lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
    1.34  
    1.35 +  def is_empty: Boolean = length == 0
    1.36 +
    1.37 +  def iterator: Iterator[Byte] =
    1.38 +    for (i <- (offset until (offset + length)).iterator)
    1.39 +      yield bytes(i)
    1.40 +
    1.41    def array: Array[Byte] =
    1.42    {
    1.43      val a = new Array[Byte](length)
    1.44 @@ -190,6 +175,13 @@
    1.45      else throw new IndexOutOfBoundsException
    1.46    }
    1.47  
    1.48 +  def trim_line: Bytes =
    1.49 +    if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
    1.50 +      subSequence(0, length - 2)
    1.51 +    else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
    1.52 +      subSequence(0, length - 1)
    1.53 +    else this
    1.54 +
    1.55  
    1.56    /* streams */
    1.57  
     2.1 --- a/src/Pure/General/symbol.scala	Mon Dec 10 23:36:29 2018 +0100
     2.2 +++ b/src/Pure/General/symbol.scala	Tue Dec 11 19:25:35 2018 +0100
     2.3 @@ -48,6 +48,8 @@
     2.4  
     2.5    def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c)
     2.6  
     2.7 +  def is_ascii_line_terminator(c: Char): Boolean = "\r\n".contains(c)
     2.8 +
     2.9    def is_ascii_letdig(c: Char): Boolean =
    2.10      is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
    2.11  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/PIDE/byte_message.ML	Tue Dec 11 19:25:35 2018 +0100
     3.3 @@ -0,0 +1,31 @@
     3.4 +(*  Title:      Pure/General/byte_message.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Byte-oriented messages.
     3.8 +*)
     3.9 +
    3.10 +signature BYTE_MESSAGE =
    3.11 +sig
    3.12 +  val read_line: BinIO.instream -> string option
    3.13 +  val read_block: BinIO.instream -> int -> string
    3.14 +end;
    3.15 +
    3.16 +structure Byte_Message: BYTE_MESSAGE =
    3.17 +struct
    3.18 +
    3.19 +fun read_line stream =
    3.20 +  let
    3.21 +    val result = trim_line o String.implode o rev;
    3.22 +    fun read cs =
    3.23 +      (case BinIO.input1 stream of
    3.24 +        NONE => if null cs then NONE else SOME (result cs)
    3.25 +      | SOME b =>
    3.26 +          (case Byte.byteToChar b of
    3.27 +            #"\n" => SOME (result cs)
    3.28 +          | c => read (c :: cs)));
    3.29 +  in read [] end;
    3.30 +
    3.31 +fun read_block stream n =
    3.32 +  Byte.bytesToString (BinIO.inputN (stream, n));
    3.33 +
    3.34 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/PIDE/byte_message.scala	Tue Dec 11 19:25:35 2018 +0100
     4.3 @@ -0,0 +1,74 @@
     4.4 +/*  Title:      Pure/General/byte_message.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Byte-oriented messages.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +import java.io.{ByteArrayOutputStream, OutputStream, InputStream, IOException}
    4.13 +
    4.14 +
    4.15 +object Byte_Message
    4.16 +{
    4.17 +  def read_line(stream: InputStream): Option[Bytes] =
    4.18 +  {
    4.19 +    val line = new ByteArrayOutputStream(100)
    4.20 +    var c = 0
    4.21 +    while ({ c = stream.read; c != -1 && c != 10 }) line.write(c)
    4.22 +
    4.23 +    if (c == -1 && line.size == 0) None
    4.24 +    else {
    4.25 +      val a = line.toByteArray
    4.26 +      val n = a.length
    4.27 +      val len = if (n > 0 && a(n - 1) == 13) n - 1 else n
    4.28 +      Some(Bytes(a, 0, len))
    4.29 +    }
    4.30 +  }
    4.31 +
    4.32 +  def read_block(stream: InputStream, length: Int): Option[Bytes] =
    4.33 +  {
    4.34 +    val msg = Bytes.read_stream(stream, limit = length)
    4.35 +    if (msg.length == length) Some(msg) else None
    4.36 +  }
    4.37 +
    4.38 +
    4.39 +  /* hybrid messages: line or length+block, with content restriction */
    4.40 +
    4.41 +  private def is_length(msg: Bytes): Boolean =
    4.42 +    !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
    4.43 +
    4.44 +  private def has_line_terminator(msg: Bytes): Boolean =
    4.45 +  {
    4.46 +    val len = msg.length
    4.47 +    len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1))
    4.48 +  }
    4.49 +
    4.50 +  def write_line_message(stream: OutputStream, msg: Bytes)
    4.51 +  {
    4.52 +    if (is_length(msg) || has_line_terminator(msg))
    4.53 +      error ("Bad content for line message:\n" ++ msg.text.take(100))
    4.54 +
    4.55 +    if (msg.length > 100 || msg.iterator.contains(10)) {
    4.56 +      stream.write(UTF8.bytes((msg.length + 1).toString))
    4.57 +      stream.write(10)
    4.58 +    }
    4.59 +    msg.write_stream(stream)
    4.60 +    stream.write(10)
    4.61 +
    4.62 +    try { stream.flush() } catch { case _: IOException => }
    4.63 +  }
    4.64 +
    4.65 +  def read_line_message(stream: InputStream): Option[Bytes] =
    4.66 +  {
    4.67 +    try {
    4.68 +      read_line(stream) match {
    4.69 +        case Some(line) =>
    4.70 +          if (is_length(line)) read_block(stream, Value.Int.parse(line.text)).map(_.trim_line)
    4.71 +          else Some(line)
    4.72 +        case None => None
    4.73 +      }
    4.74 +    }
    4.75 +    catch { case _: IOException => None }
    4.76 +  }
    4.77 +}
     5.1 --- a/src/Pure/ROOT.ML	Mon Dec 10 23:36:29 2018 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Tue Dec 11 19:25:35 2018 +0100
     5.3 @@ -83,12 +83,12 @@
     5.4  ML_file "General/file.ML";
     5.5  ML_file "General/long_name.ML";
     5.6  ML_file "General/binding.ML";
     5.7 -ML_file "General/bytes.ML";
     5.8  ML_file "General/socket_io.ML";
     5.9  ML_file "General/seq.ML";
    5.10  ML_file "General/timing.ML";
    5.11  ML_file "General/sha1.ML";
    5.12  
    5.13 +ML_file "PIDE/byte_message.ML";
    5.14  ML_file "PIDE/yxml.ML";
    5.15  ML_file "PIDE/document_id.ML";
    5.16  
     6.1 --- a/src/Pure/System/system_channel.ML	Mon Dec 10 23:36:29 2018 +0100
     6.2 +++ b/src/Pure/System/system_channel.ML	Tue Dec 11 19:25:35 2018 +0100
     6.3 @@ -19,8 +19,8 @@
     6.4  
     6.5  datatype T = System_Channel of BinIO.instream * BinIO.outstream;
     6.6  
     6.7 -fun input_line (System_Channel (stream, _)) = Bytes.read_line stream;
     6.8 -fun inputN (System_Channel (stream, _)) n = Bytes.read_block stream n;
     6.9 +fun input_line (System_Channel (stream, _)) = Byte_Message.read_line stream;
    6.10 +fun inputN (System_Channel (stream, _)) n = Byte_Message.read_block stream n;
    6.11  
    6.12  fun output (System_Channel (_, stream)) s = File.output stream s;
    6.13  fun flush (System_Channel (_, stream)) = BinIO.flushOut stream;
     7.1 --- a/src/Pure/Tools/server.scala	Mon Dec 10 23:36:29 2018 +0100
     7.2 +++ b/src/Pure/Tools/server.scala	Tue Dec 11 19:25:35 2018 +0100
     7.3 @@ -181,26 +181,10 @@
     7.4          interrupt = interrupt)
     7.5  
     7.6      def read_message(): Option[String] =
     7.7 -      try {
     7.8 -        Bytes.read_line(in).map(_.text) match {
     7.9 -          case Some(Value.Int(n)) =>
    7.10 -            Bytes.read_block(in, n).map(bytes => Library.trim_line(bytes.text))
    7.11 -          case res => res
    7.12 -        }
    7.13 -      }
    7.14 -      catch { case _: SocketException => None }
    7.15 +      Byte_Message.read_line_message(in).map(_.text)
    7.16  
    7.17 -    def write_message(msg: String): Unit = out_lock.synchronized
    7.18 -    {
    7.19 -      val b = UTF8.bytes(msg)
    7.20 -      if (b.length > 100 || b.contains(10)) {
    7.21 -        out.write(UTF8.bytes((b.length + 1).toString))
    7.22 -        out.write(10)
    7.23 -      }
    7.24 -      out.write(b)
    7.25 -      out.write(10)
    7.26 -      try { out.flush() } catch { case _: SocketException => }
    7.27 -    }
    7.28 +    def write_message(msg: String): Unit =
    7.29 +      out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
    7.30  
    7.31      def reply(r: Reply.Value, arg: Any)
    7.32      {
     8.1 --- a/src/Pure/build-jars	Mon Dec 10 23:36:29 2018 +0100
     8.2 +++ b/src/Pure/build-jars	Tue Dec 11 19:25:35 2018 +0100
     8.3 @@ -89,6 +89,7 @@
     8.4    ML/ml_process.scala
     8.5    ML/ml_statistics.scala
     8.6    ML/ml_syntax.scala
     8.7 +  PIDE/byte_message.scala
     8.8    PIDE/command.scala
     8.9    PIDE/command_span.scala
    8.10    PIDE/document.scala
     9.1 --- a/src/Tools/Haskell/Haskell.thy	Mon Dec 10 23:36:29 2018 +0100
     9.2 +++ b/src/Tools/Haskell/Haskell.thy	Tue Dec 11 19:25:35 2018 +0100
     9.3 @@ -1368,15 +1368,18 @@
     9.4      \([], a) -> App (pair term term a)]
     9.5  \<close>
     9.6  
     9.7 -generate_file "Isabelle/Bytes.hs" = \<open>
     9.8 -{-  Title:      Isabelle/Bytes.hs
     9.9 +generate_file "Isabelle/Byte_Message.hs" = \<open>
    9.10 +{-  Title:      Isabelle/Byte_Message.hs
    9.11      Author:     Makarius
    9.12      LICENSE:    BSD 3-clause (Isabelle)
    9.13  
    9.14 -Byte-vector messages.
    9.15 +Byte-oriented messages.
    9.16 +
    9.17 +See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\<close>
    9.18 +and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
    9.19  -}
    9.20  
    9.21 -module Isabelle.Bytes (read_line, read_block, read_message, write_message)
    9.22 +module Isabelle.Byte_Message (read_line, read_block, trim_line, read_line_message, write_line_message)
    9.23  where
    9.24  
    9.25  import Data.ByteString (ByteString)
    9.26 @@ -1384,6 +1387,7 @@
    9.27  import qualified Data.ByteString.UTF8 as UTF8
    9.28  import Data.Word (Word8)
    9.29  
    9.30 +import Control.Monad (when)
    9.31  import Network.Socket (Socket)
    9.32  import qualified Network.Socket as Socket
    9.33  import qualified Network.Socket.ByteString as ByteString
    9.34 @@ -1391,8 +1395,6 @@
    9.35  import qualified Isabelle.Value as Value
    9.36  
    9.37  
    9.38 --- see also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/bytes.ML\<close>
    9.39 -
    9.40  read_line :: Socket -> IO (Maybe ByteString)
    9.41  read_line socket = read []
    9.42    where
    9.43 @@ -1411,13 +1413,15 @@
    9.44              10 -> return (Just (result bs))
    9.45              b -> read (b : bs)
    9.46  
    9.47 -read_block :: Socket -> Int -> IO ByteString
    9.48 +read_block :: Socket -> Int -> IO (Maybe ByteString)
    9.49  read_block socket n = read 0 []
    9.50    where
    9.51 -    result :: [ByteString] -> ByteString
    9.52 -    result = ByteString.concat . reverse
    9.53 +    result :: [ByteString] -> Maybe ByteString
    9.54 +    result ss =
    9.55 +      if ByteString.length s == n then Just s else Nothing
    9.56 +      where s = ByteString.concat (reverse ss)
    9.57  
    9.58 -    read :: Int -> [ByteString] -> IO ByteString
    9.59 +    read :: Int -> [ByteString] -> IO (Maybe ByteString)
    9.60      read len ss =
    9.61        if len >= n then return (result ss)
    9.62        else
    9.63 @@ -1427,27 +1431,48 @@
    9.64              0 -> return (result ss)
    9.65              m -> read (len + m) (s : ss))
    9.66  
    9.67 +trim_line :: ByteString -> ByteString
    9.68 +trim_line s =
    9.69 +    if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then ByteString.take (n - 2) s
    9.70 +    else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then ByteString.take (n - 1) s
    9.71 +    else s
    9.72 +  where
    9.73 +    n = ByteString.length s
    9.74 +    at = ByteString.index s
    9.75  
    9.76 --- see also \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close>
    9.77 +
    9.78 +
    9.79 +-- hybrid messages: line or length+block (with content restriction)
    9.80 +
    9.81 +is_length :: ByteString -> Bool
    9.82 +is_length s =
    9.83 +  not (ByteString.null s) && ByteString.all (\b -> 48 <= b && b <= 57) s
    9.84  
    9.85 -read_message :: Socket -> IO (Maybe ByteString)
    9.86 -read_message socket = do
    9.87 +has_line_terminator :: ByteString -> Bool
    9.88 +has_line_terminator s =
    9.89 +  not (ByteString.null s) && (ByteString.last s == 13 || ByteString.last s == 10)
    9.90 +
    9.91 +write_line_message :: Socket -> ByteString -> IO ()
    9.92 +write_line_message socket msg = do
    9.93 +  when (is_length msg || has_line_terminator msg) $
    9.94 +    error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
    9.95 +
    9.96 +  let newline = ByteString.singleton 10
    9.97 +  let n = ByteString.length msg
    9.98 +  ByteString.sendMany socket
    9.99 +    (if n > 100 || ByteString.any (== 10) msg then
   9.100 +      [UTF8.fromString (Value.print_int (n + 1)), newline, msg, newline]
   9.101 +     else [msg, newline])
   9.102 +
   9.103 +read_line_message :: Socket -> IO (Maybe ByteString)
   9.104 +read_line_message socket = do
   9.105    opt_line <- read_line socket
   9.106    case opt_line of
   9.107      Nothing -> return Nothing
   9.108      Just line ->
   9.109        case Value.parse_int (UTF8.toString line) of
   9.110          Nothing -> return $ Just line
   9.111 -        Just n -> Just <$> read_block socket n
   9.112 -
   9.113 -write_message :: Socket -> ByteString -> IO ()
   9.114 -write_message socket msg = do
   9.115 -  let newline = ByteString.singleton 10
   9.116 -  let n = ByteString.length msg
   9.117 -  ByteString.sendMany socket
   9.118 -    (if n > 100 || ByteString.any (== 10) msg then
   9.119 -      [UTF8.fromString (Value.print_int (n + 1)), newline, msg, newline]
   9.120 -     else [msg, newline])
   9.121 +        Just n -> fmap trim_line <$> read_block socket n
   9.122  \<close>
   9.123  
   9.124  end
    10.1 --- a/src/Tools/VSCode/src/channel.scala	Mon Dec 10 23:36:29 2018 +0100
    10.2 +++ b/src/Tools/VSCode/src/channel.scala	Tue Dec 11 19:25:35 2018 +0100
    10.3 @@ -21,7 +21,7 @@
    10.4    private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
    10.5  
    10.6    private def read_line(): String =
    10.7 -    Bytes.read_line(in) match {
    10.8 +    Byte_Message.read_line(in) match {
    10.9        case Some(bytes) => bytes.text
   10.10        case None => ""
   10.11      }