69448
|
1 |
/* Title: Pure/General/byte_message.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Byte-oriented messages.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
import java.io.{ByteArrayOutputStream, OutputStream, InputStream, IOException}
|
|
10 |
|
|
11 |
|
|
12 |
object Byte_Message
|
|
13 |
{
|
|
14 |
def read_line(stream: InputStream): Option[Bytes] =
|
|
15 |
{
|
|
16 |
val line = new ByteArrayOutputStream(100)
|
|
17 |
var c = 0
|
|
18 |
while ({ c = stream.read; c != -1 && c != 10 }) line.write(c)
|
|
19 |
|
|
20 |
if (c == -1 && line.size == 0) None
|
|
21 |
else {
|
|
22 |
val a = line.toByteArray
|
|
23 |
val n = a.length
|
|
24 |
val len = if (n > 0 && a(n - 1) == 13) n - 1 else n
|
|
25 |
Some(Bytes(a, 0, len))
|
|
26 |
}
|
|
27 |
}
|
|
28 |
|
|
29 |
def read_block(stream: InputStream, length: Int): Option[Bytes] =
|
|
30 |
{
|
|
31 |
val msg = Bytes.read_stream(stream, limit = length)
|
|
32 |
if (msg.length == length) Some(msg) else None
|
|
33 |
}
|
|
34 |
|
|
35 |
|
|
36 |
/* hybrid messages: line or length+block, with content restriction */
|
|
37 |
|
|
38 |
private def is_length(msg: Bytes): Boolean =
|
|
39 |
!msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
|
|
40 |
|
|
41 |
private def has_line_terminator(msg: Bytes): Boolean =
|
|
42 |
{
|
|
43 |
val len = msg.length
|
|
44 |
len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1))
|
|
45 |
}
|
|
46 |
|
|
47 |
def write_line_message(stream: OutputStream, msg: Bytes)
|
|
48 |
{
|
|
49 |
if (is_length(msg) || has_line_terminator(msg))
|
|
50 |
error ("Bad content for line message:\n" ++ msg.text.take(100))
|
|
51 |
|
|
52 |
if (msg.length > 100 || msg.iterator.contains(10)) {
|
|
53 |
stream.write(UTF8.bytes((msg.length + 1).toString))
|
|
54 |
stream.write(10)
|
|
55 |
}
|
|
56 |
msg.write_stream(stream)
|
|
57 |
stream.write(10)
|
|
58 |
|
|
59 |
try { stream.flush() } catch { case _: IOException => }
|
|
60 |
}
|
|
61 |
|
|
62 |
def read_line_message(stream: InputStream): Option[Bytes] =
|
|
63 |
{
|
|
64 |
try {
|
|
65 |
read_line(stream) match {
|
|
66 |
case Some(line) =>
|
|
67 |
if (is_length(line)) read_block(stream, Value.Int.parse(line.text)).map(_.trim_line)
|
|
68 |
else Some(line)
|
|
69 |
case None => None
|
|
70 |
}
|
|
71 |
}
|
|
72 |
catch { case _: IOException => None }
|
|
73 |
}
|
|
74 |
}
|