src/Pure/PIDE/byte_message.scala
changeset 80362 d395b7e14102
parent 80357 fe123d033e76
child 80386 10f47bb1abd3
equal deleted inserted replaced
80361:54a83e8e447b 80362:d395b7e14102
    77 
    77 
    78 
    78 
    79   /* hybrid messages: line or length+block (restricted content) */
    79   /* hybrid messages: line or length+block (restricted content) */
    80 
    80 
    81   private def is_length(msg: Bytes): Boolean =
    81   private def is_length(msg: Bytes): Boolean =
    82     !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
    82     !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
    83 
    83 
    84   private def is_terminated(msg: Bytes): Boolean =
    84   private def is_terminated(msg: Bytes): Boolean =
    85     msg.size match {
    85     msg.size match {
    86       case size if size > 0 =>
    86       case size if size > 0 =>
    87         val c = msg(size - 1)
    87         val c = msg(size - 1)
    93     if (is_length(msg) || is_terminated(msg))
    93     if (is_length(msg) || is_terminated(msg))
    94       error ("Bad content for line message:\n" ++ msg.text.take(100))
    94       error ("Bad content for line message:\n" ++ msg.text.take(100))
    95 
    95 
    96     val n = msg.size
    96     val n = msg.size
    97     write(stream,
    97     write(stream,
    98       (if (n > 100 || msg.iterator.contains(10)) make_header(List(n + 1)) else Nil) :::
    98       (if (n > 100 || msg.byte_iterator.contains(10)) make_header(List(n + 1)) else Nil) :::
    99         List(msg, Bytes.newline))
    99         List(msg, Bytes.newline))
   100     flush(stream)
   100     flush(stream)
   101   }
   101   }
   102 
   102 
   103   def read_line_message(stream: InputStream): Option[Bytes] =
   103   def read_line_message(stream: InputStream): Option[Bytes] =