author | wenzelm |
Sat, 28 Nov 2020 20:14:46 +0100 | |
changeset 72761 | 4519eeefe3b5 |
parent 71774 | 491f185fd705 |
child 73340 | 0ffcad1f6130 |
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 = |
|
69448 | 24 |
Byte_Message.read_line(in) match { |
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
25 |
case Some(bytes) => bytes.text |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
26 |
case None => "" |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
27 |
} |
64605 | 28 |
|
29 |
private def read_header(): List[String] = |
|
30 |
{ |
|
31 |
val header = new mutable.ListBuffer[String] |
|
32 |
var line = "" |
|
33 |
while ({ line = read_line(); line != "" }) header += line |
|
34 |
header.toList |
|
35 |
} |
|
36 |
||
37 |
private def read_content(n: Int): String = |
|
38 |
{ |
|
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
39 |
val bytes = Bytes.read_stream(in, limit = n) |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
40 |
if (bytes.length == n) bytes.text |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
41 |
else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)") |
64605 | 42 |
} |
43 |
||
44 |
def read(): Option[JSON.T] = |
|
45 |
{ |
|
46 |
read_header() match { |
|
47 |
case Nil => None |
|
48 |
case Content_Length(s) :: _ => |
|
49 |
s match { |
|
50 |
case Value.Int(n) if n >= 0 => |
|
51 |
val msg = read_content(n) |
|
65922 | 52 |
val json = JSON.parse(msg) |
72761 | 53 |
LSP.Message.log("IN: " + n, json, log, verbose) |
65922 | 54 |
Some(json) |
64605 | 55 |
case _ => error("Bad Content-Length: " + s) |
56 |
} |
|
57 |
case header => error(cat_lines("Malformed header:" :: header)) |
|
58 |
} |
|
59 |
} |
|
60 |
||
61 |
||
62 |
/* write message */ |
|
63 |
||
64 |
def write(json: JSON.T) |
|
65 |
{ |
|
66 |
val msg = JSON.Format(json) |
|
65152 | 67 |
val content = UTF8.bytes(msg) |
68 |
val n = content.length |
|
69 |
val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n") |
|
64605 | 70 |
|
72761 | 71 |
LSP.Message.log("OUT: " + n, json, log, verbose) |
64605 | 72 |
out.synchronized { |
73 |
out.write(header) |
|
74 |
out.write(content) |
|
75 |
out.flush |
|
76 |
} |
|
77 |
} |
|
64642
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
78 |
|
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
79 |
|
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
80 |
/* display message */ |
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
81 |
|
64686 | 82 |
def display_message(message_type: Int, msg: String, show: Boolean = true): Unit = |
72761 | 83 |
write(LSP.DisplayMessage(message_type, Output.clean_yxml(msg), show)) |
64642
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
84 |
|
72761 | 85 |
def error_message(msg: String) { display_message(LSP.MessageType.Error, msg, true) } |
86 |
def warning(msg: String) { display_message(LSP.MessageType.Warning, msg, true) } |
|
87 |
def writeln(msg: String) { display_message(LSP.MessageType.Info, msg, true) } |
|
64686 | 88 |
|
72761 | 89 |
def log_error_message(msg: String) { display_message(LSP.MessageType.Error, msg, false) } |
90 |
def log_warning(msg: String) { display_message(LSP.MessageType.Warning, msg, false) } |
|
91 |
def log_writeln(msg: String) { display_message(LSP.MessageType.Info, msg, false) } |
|
64675 | 92 |
|
64810 | 93 |
object Error_Logger extends Logger |
94 |
{ |
|
95 |
def apply(msg: => String) { log_error_message(msg) } |
|
96 |
} |
|
97 |
||
64675 | 98 |
|
64733 | 99 |
/* progress */ |
100 |
||
67856 | 101 |
def progress(verbose: Boolean = false): Progress = |
64733 | 102 |
new Progress { |
103 |
override def echo(msg: String): Unit = log_writeln(msg) |
|
65829 | 104 |
override def echo_warning(msg: String): Unit = log_warning(msg) |
105 |
override def echo_error_message(msg: String): Unit = log_error_message(msg) |
|
68957 | 106 |
override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message) |
64733 | 107 |
} |
64605 | 108 |
} |