src/Pure/PIDE/byte_message.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 69477 e8893c893241
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm@69458
     1
/*  Title:      Pure/General/byte_message.scala
wenzelm@69458
     2
    Author:     Makarius
wenzelm@69458
     3
wenzelm@69458
     4
Byte-oriented messages.
wenzelm@69458
     5
*/
wenzelm@69458
     6
wenzelm@69458
     7
package isabelle
wenzelm@69458
     8
wenzelm@69458
     9
import java.io.{ByteArrayOutputStream, OutputStream, InputStream, IOException}
wenzelm@69458
    10
wenzelm@69458
    11
wenzelm@69458
    12
object Byte_Message
wenzelm@69458
    13
{
wenzelm@69461
    14
  /* output operations */
wenzelm@69461
    15
wenzelm@69464
    16
  def write(stream: OutputStream, bytes: List[Bytes]): Unit =
wenzelm@69464
    17
    bytes.foreach(_.write_stream(stream))
wenzelm@69461
    18
wenzelm@69461
    19
  def flush(stream: OutputStream): Unit =
wenzelm@69461
    20
    try { stream.flush() }
wenzelm@69461
    21
    catch { case _: IOException => }
wenzelm@69461
    22
wenzelm@69477
    23
  def write_line(stream: OutputStream, bytes: Bytes): Unit =
wenzelm@69477
    24
  {
wenzelm@69477
    25
    write(stream, List(bytes, Bytes.newline))
wenzelm@69477
    26
    flush(stream)
wenzelm@69477
    27
  }
wenzelm@69477
    28
wenzelm@69461
    29
wenzelm@69461
    30
  /* input operations */
wenzelm@69461
    31
wenzelm@69462
    32
  def read(stream: InputStream, n: Int): Bytes =
wenzelm@69462
    33
    Bytes.read_stream(stream, limit = n)
wenzelm@69459
    34
wenzelm@69462
    35
  def read_block(stream: InputStream, n: Int): (Option[Bytes], Int) =
wenzelm@69459
    36
  {
wenzelm@69462
    37
    val msg = read(stream, n)
wenzelm@69462
    38
    val len = msg.length
wenzelm@69462
    39
    (if (len == n) Some(msg) else None, len)
wenzelm@69459
    40
  }
wenzelm@69459
    41
wenzelm@69458
    42
  def read_line(stream: InputStream): Option[Bytes] =
wenzelm@69458
    43
  {
wenzelm@69458
    44
    val line = new ByteArrayOutputStream(100)
wenzelm@69458
    45
    var c = 0
wenzelm@69458
    46
    while ({ c = stream.read; c != -1 && c != 10 }) line.write(c)
wenzelm@69458
    47
wenzelm@69458
    48
    if (c == -1 && line.size == 0) None
wenzelm@69458
    49
    else {
wenzelm@69458
    50
      val a = line.toByteArray
wenzelm@69458
    51
      val n = a.length
wenzelm@69458
    52
      val len = if (n > 0 && a(n - 1) == 13) n - 1 else n
wenzelm@69458
    53
      Some(Bytes(a, 0, len))
wenzelm@69458
    54
    }
wenzelm@69458
    55
  }
wenzelm@69458
    56
wenzelm@69458
    57
wenzelm@69464
    58
  /* messages with multiple chunks (arbitrary content) */
wenzelm@69461
    59
wenzelm@69464
    60
  private def make_header(ns: List[Int]): List[Bytes] =
wenzelm@69464
    61
    List(Bytes(ns.mkString(",")), Bytes.newline)
wenzelm@69464
    62
wenzelm@69464
    63
  def write_message(stream: OutputStream, chunks: List[Bytes])
wenzelm@69462
    64
  {
wenzelm@69464
    65
    write(stream, make_header(chunks.map(_.length)) ::: chunks)
wenzelm@69464
    66
    flush(stream)
wenzelm@69462
    67
  }
wenzelm@69462
    68
wenzelm@69461
    69
  private def parse_header(line: String): List[Int] =
wenzelm@69462
    70
    try { space_explode(',', line).map(Value.Nat.parse) }
wenzelm@69464
    71
    catch { case ERROR(_) => error("Malformed message header: " + quote(line)) }
wenzelm@69461
    72
wenzelm@69461
    73
  private def read_chunk(stream: InputStream, n: Int): Bytes =
wenzelm@69462
    74
    read_block(stream, n) match {
wenzelm@69462
    75
      case (Some(chunk), _) => chunk
wenzelm@69462
    76
      case (None, len) =>
wenzelm@69462
    77
        error("Malformed message chunk: unexpected EOF after " + len + " of " + n + " bytes")
wenzelm@69462
    78
    }
wenzelm@69461
    79
wenzelm@69461
    80
  def read_message(stream: InputStream): Option[List[Bytes]] =
wenzelm@69464
    81
    read_line(stream).map(line => parse_header(line.text).map(read_chunk(stream, _)))
wenzelm@69461
    82
wenzelm@69461
    83
wenzelm@69461
    84
  /* hybrid messages: line or length+block (restricted content) */
wenzelm@69458
    85
wenzelm@69458
    86
  private def is_length(msg: Bytes): Boolean =
wenzelm@69458
    87
    !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
wenzelm@69458
    88
wenzelm@69462
    89
  private def is_terminated(msg: Bytes): Boolean =
wenzelm@69458
    90
  {
wenzelm@69458
    91
    val len = msg.length
wenzelm@69458
    92
    len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1))
wenzelm@69458
    93
  }
wenzelm@69458
    94
wenzelm@69458
    95
  def write_line_message(stream: OutputStream, msg: Bytes)
wenzelm@69458
    96
  {
wenzelm@69462
    97
    if (is_length(msg) || is_terminated(msg))
wenzelm@69458
    98
      error ("Bad content for line message:\n" ++ msg.text.take(100))
wenzelm@69458
    99
wenzelm@69462
   100
    val n = msg.length
wenzelm@69464
   101
    write(stream,
wenzelm@69464
   102
      (if (n > 100 || msg.iterator.contains(10)) make_header(List(n + 1)) else Nil) :::
wenzelm@69464
   103
        List(msg, Bytes.newline))
wenzelm@69461
   104
    flush(stream)
wenzelm@69458
   105
  }
wenzelm@69458
   106
wenzelm@69458
   107
  def read_line_message(stream: InputStream): Option[Bytes] =
wenzelm@69461
   108
    read_line(stream) match {
wenzelm@69462
   109
      case None => None
wenzelm@69461
   110
      case Some(line) =>
wenzelm@69462
   111
        Value.Nat.unapply(line.text) match {
wenzelm@69462
   112
          case None => Some(line)
wenzelm@69462
   113
          case Some(n) => read_block(stream, n)._1.map(_.trim_line)
wenzelm@69462
   114
        }
wenzelm@69458
   115
    }
wenzelm@69458
   116
}