src/Pure/PIDE/byte_message.scala
changeset 80549 769a52499f12
parent 80548 d1662f1296db
equal deleted inserted replaced
80548:d1662f1296db 80549:769a52499f12
    42       Bytes.Builder.use(hint = 100) { builder =>
    42       Bytes.Builder.use(hint = 100) { builder =>
    43         while ({ c = stream.read; c != -1 && c != 10 }) {
    43         while ({ c = stream.read; c != -1 && c != 10 }) {
    44           builder += c.toByte
    44           builder += c.toByte
    45         }
    45         }
    46       }
    46       }
    47     if (c == -1 && line.size == 0) None else Some(line.trim_line)
    47     if (c == -1 && line.is_empty) None else Some(line.trim_line)
    48   }
    48   }
    49 
    49 
    50 
    50 
    51   /* messages with multiple chunks (arbitrary content) */
    51   /* messages with multiple chunks (arbitrary content) */
    52 
    52