src/Pure/PIDE/byte_message.scala
changeset 80493 d334f158442b
parent 80392 c22a56495b4c
child 80548 d1662f1296db
equal deleted inserted replaced
80492:43323d886ea3 80493:d334f158442b
    83 
    83 
    84   private def is_length(msg: Bytes): Boolean =
    84   private def is_length(msg: Bytes): Boolean =
    85     !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) &&
    85     !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) &&
    86       Value.Long.unapply(msg.text).isDefined
    86       Value.Long.unapply(msg.text).isDefined
    87 
    87 
    88   private def is_terminated(msg: Bytes): Boolean =
       
    89     msg.size match {
       
    90       case size if size > 0 =>
       
    91         val c = msg(size - 1)
       
    92         c <= Char.MaxValue && Symbol.is_ascii_line_terminator(c.toChar)
       
    93       case _ => false
       
    94     }
       
    95 
       
    96   def write_line_message(stream: OutputStream, msg: Bytes): Unit = {
    88   def write_line_message(stream: OutputStream, msg: Bytes): Unit = {
    97     if (is_length(msg) || is_terminated(msg)) {
    89     if (is_length(msg) || msg.terminated_line) {
    98       error ("Bad content for line message:\n" ++ msg.text.take(100))
    90       error ("Bad content for line message:\n" ++ msg.text.take(100))
    99     }
    91     }
   100 
    92 
   101     val n = msg.size
    93     val n = msg.size
   102     write(stream,
    94     write(stream,