author | wenzelm |
Fri, 30 Dec 2016 10:26:10 +0100 | |
changeset 64706 | 3ebf9f8299df |
parent 64686 | 7888be4fa496 |
child 64717 | d2b50eb3d9ab |
permissions | -rw-r--r-- |
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 |
} |
|
64642
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
89 |
|
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
90 |
|
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
91 |
/* display message */ |
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
92 |
|
64686 | 93 |
def display_message(message_type: Int, msg: String, show: Boolean = true): Unit = |
94 |
write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show)) |
|
64642
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
95 |
|
64686 | 96 |
def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) } |
97 |
def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) } |
|
98 |
def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) } |
|
99 |
||
100 |
def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) } |
|
101 |
def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) } |
|
102 |
def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) } |
|
64675 | 103 |
|
104 |
||
105 |
/* diagnostics */ |
|
106 |
||
107 |
def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit = |
|
108 |
write(Protocol.PublishDiagnostics(uri, diagnostics)) |
|
64605 | 109 |
} |