author | wenzelm |
Thu, 25 May 2017 18:07:29 +0200 | |
changeset 65922 | d2f19f05c0e9 |
parent 65829 | 07e86b942a84 |
child 67805 | 2d9a265b294e |
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 |
||
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64733
diff
changeset
|
12 |
import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream, File => JFile} |
64605 | 13 |
|
14 |
import scala.collection.mutable |
|
15 |
||
16 |
||
65922 | 17 |
class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger, verbose: Boolean = false) |
64605 | 18 |
{ |
19 |
/* read message */ |
|
20 |
||
21 |
private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r |
|
22 |
||
23 |
private def read_line(): String = |
|
24 |
{ |
|
25 |
val buffer = new ByteArrayOutputStream(100) |
|
26 |
var c = 0 |
|
27 |
while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c) |
|
28 |
Library.trim_line(buffer.toString(UTF8.charset_name)) |
|
29 |
} |
|
30 |
||
31 |
private def read_header(): List[String] = |
|
32 |
{ |
|
33 |
val header = new mutable.ListBuffer[String] |
|
34 |
var line = "" |
|
35 |
while ({ line = read_line(); line != "" }) header += line |
|
36 |
header.toList |
|
37 |
} |
|
38 |
||
39 |
private def read_content(n: Int): String = |
|
40 |
{ |
|
41 |
val buffer = new Array[Byte](n) |
|
42 |
var i = 0 |
|
43 |
var m = 0 |
|
44 |
do { |
|
45 |
m = in.read(buffer, i, n - i) |
|
46 |
if (m != -1) i += m |
|
47 |
} |
|
48 |
while (m != -1 && n > i) |
|
49 |
||
50 |
if (i == n) new String(buffer, UTF8.charset) |
|
51 |
else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)") |
|
52 |
} |
|
53 |
||
54 |
def read(): Option[JSON.T] = |
|
55 |
{ |
|
56 |
read_header() match { |
|
57 |
case Nil => None |
|
58 |
case Content_Length(s) :: _ => |
|
59 |
s match { |
|
60 |
case Value.Int(n) if n >= 0 => |
|
61 |
val msg = read_content(n) |
|
65922 | 62 |
val json = JSON.parse(msg) |
63 |
Protocol.Message.log("IN: " + n, json, log, verbose) |
|
64 |
Some(json) |
|
64605 | 65 |
case _ => error("Bad Content-Length: " + s) |
66 |
} |
|
67 |
case header => error(cat_lines("Malformed header:" :: header)) |
|
68 |
} |
|
69 |
} |
|
70 |
||
71 |
||
72 |
/* write message */ |
|
73 |
||
74 |
def write(json: JSON.T) |
|
75 |
{ |
|
76 |
val msg = JSON.Format(json) |
|
65152 | 77 |
val content = UTF8.bytes(msg) |
78 |
val n = content.length |
|
79 |
val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n") |
|
64605 | 80 |
|
65922 | 81 |
Protocol.Message.log("OUT: " + n, json, log, verbose) |
64605 | 82 |
out.synchronized { |
83 |
out.write(header) |
|
84 |
out.write(content) |
|
85 |
out.flush |
|
86 |
} |
|
87 |
} |
|
64642
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
88 |
|
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 |
/* display message */ |
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
91 |
|
64686 | 92 |
def display_message(message_type: Int, msg: String, show: Boolean = true): Unit = |
93 |
write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show)) |
|
64642
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
94 |
|
64686 | 95 |
def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) } |
96 |
def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) } |
|
97 |
def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) } |
|
98 |
||
99 |
def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) } |
|
100 |
def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) } |
|
101 |
def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) } |
|
64675 | 102 |
|
64810 | 103 |
object Error_Logger extends Logger |
104 |
{ |
|
105 |
def apply(msg: => String) { log_error_message(msg) } |
|
106 |
} |
|
107 |
||
64675 | 108 |
|
64733 | 109 |
/* progress */ |
110 |
||
111 |
def make_progress(verbose: Boolean = false): Progress = |
|
112 |
new Progress { |
|
113 |
override def echo(msg: String): Unit = log_writeln(msg) |
|
65829 | 114 |
override def echo_warning(msg: String): Unit = log_warning(msg) |
115 |
override def echo_error_message(msg: String): Unit = log_error_message(msg) |
|
64733 | 116 |
override def theory(session: String, theory: String): Unit = |
117 |
if (verbose) echo(session + ": theory " + theory) |
|
118 |
} |
|
64605 | 119 |
} |