64605
|
1 |
/* Title: Tools/VSCode/src/channel.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Channel with JSON RPC protocol.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.vscode
|
|
8 |
|
|
9 |
|
|
10 |
import isabelle._
|
|
11 |
|
|
12 |
import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream}
|
|
13 |
|
|
14 |
import scala.collection.mutable
|
|
15 |
|
|
16 |
|
|
17 |
class Channel(in: InputStream, out: OutputStream, log_file: Option[Path] = None)
|
|
18 |
{
|
|
19 |
val log: Logger = Logger.make(log_file)
|
|
20 |
|
|
21 |
|
|
22 |
/* read message */
|
|
23 |
|
|
24 |
private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
|
|
25 |
|
|
26 |
private def read_line(): String =
|
|
27 |
{
|
|
28 |
val buffer = new ByteArrayOutputStream(100)
|
|
29 |
var c = 0
|
|
30 |
while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
|
|
31 |
Library.trim_line(buffer.toString(UTF8.charset_name))
|
|
32 |
}
|
|
33 |
|
|
34 |
private def read_header(): List[String] =
|
|
35 |
{
|
|
36 |
val header = new mutable.ListBuffer[String]
|
|
37 |
var line = ""
|
|
38 |
while ({ line = read_line(); line != "" }) header += line
|
|
39 |
header.toList
|
|
40 |
}
|
|
41 |
|
|
42 |
private def read_content(n: Int): String =
|
|
43 |
{
|
|
44 |
val buffer = new Array[Byte](n)
|
|
45 |
var i = 0
|
|
46 |
var m = 0
|
|
47 |
do {
|
|
48 |
m = in.read(buffer, i, n - i)
|
|
49 |
if (m != -1) i += m
|
|
50 |
}
|
|
51 |
while (m != -1 && n > i)
|
|
52 |
|
|
53 |
if (i == n) new String(buffer, UTF8.charset)
|
|
54 |
else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
|
|
55 |
}
|
|
56 |
|
|
57 |
def read(): Option[JSON.T] =
|
|
58 |
{
|
|
59 |
read_header() match {
|
|
60 |
case Nil => None
|
|
61 |
case Content_Length(s) :: _ =>
|
|
62 |
s match {
|
|
63 |
case Value.Int(n) if n >= 0 =>
|
|
64 |
val msg = read_content(n)
|
|
65 |
log("IN:\n" + msg)
|
|
66 |
Some(JSON.parse(msg))
|
|
67 |
case _ => error("Bad Content-Length: " + s)
|
|
68 |
}
|
|
69 |
case header => error(cat_lines("Malformed header:" :: header))
|
|
70 |
}
|
|
71 |
}
|
|
72 |
|
|
73 |
|
|
74 |
/* write message */
|
|
75 |
|
|
76 |
def write(json: JSON.T)
|
|
77 |
{
|
|
78 |
val msg = JSON.Format(json)
|
|
79 |
log("OUT:\n" + msg)
|
|
80 |
|
|
81 |
val content = UTF8.bytes(msg)
|
|
82 |
val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n")
|
|
83 |
out.synchronized {
|
|
84 |
out.write(header)
|
|
85 |
out.write(content)
|
|
86 |
out.flush
|
|
87 |
}
|
|
88 |
}
|
|
89 |
}
|