author | wenzelm |
Sat, 04 Mar 2023 21:41:16 +0100 | |
changeset 77508 | 7d13996ffecc |
parent 77502 | 2e2b2bd6b2d2 |
child 77509 | 3bc49507bae5 |
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 |
||
75393 | 17 |
class Channel( |
18 |
in: InputStream, |
|
19 |
out: OutputStream, |
|
20 |
log: Logger = No_Logger, |
|
21 |
verbose: Boolean = false |
|
22 |
) { |
|
64605 | 23 |
/* read message */ |
24 |
||
25 |
private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r |
|
26 |
||
27 |
private def read_line(): String = |
|
69448 | 28 |
Byte_Message.read_line(in) match { |
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
29 |
case Some(bytes) => bytes.text |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
30 |
case None => "" |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
31 |
} |
64605 | 32 |
|
75393 | 33 |
private def read_header(): List[String] = { |
64605 | 34 |
val header = new mutable.ListBuffer[String] |
35 |
var line = "" |
|
36 |
while ({ line = read_line(); line != "" }) header += line |
|
37 |
header.toList |
|
38 |
} |
|
39 |
||
75393 | 40 |
private def read_content(n: Int): String = { |
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
41 |
val bytes = Bytes.read_stream(in, limit = n) |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
42 |
if (bytes.length == n) bytes.text |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
65922
diff
changeset
|
43 |
else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)") |
64605 | 44 |
} |
45 |
||
75393 | 46 |
def read(): Option[JSON.T] = { |
64605 | 47 |
read_header() match { |
48 |
case Nil => None |
|
49 |
case Content_Length(s) :: _ => |
|
50 |
s match { |
|
51 |
case Value.Int(n) if n >= 0 => |
|
52 |
val msg = read_content(n) |
|
65922 | 53 |
val json = JSON.parse(msg) |
72761 | 54 |
LSP.Message.log("IN: " + n, json, log, verbose) |
65922 | 55 |
Some(json) |
64605 | 56 |
case _ => error("Bad Content-Length: " + s) |
57 |
} |
|
58 |
case header => error(cat_lines("Malformed header:" :: header)) |
|
59 |
} |
|
60 |
} |
|
61 |
||
62 |
||
63 |
/* write message */ |
|
64 |
||
75393 | 65 |
def write(json: JSON.T): Unit = { |
64605 | 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 |
|
73541 | 82 |
def display_message(message_type: Int, msg: String, show: Boolean): Unit = |
77498
2d12cb7ff829
proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;
wenzelm
parents:
75393
diff
changeset
|
83 |
write(LSP.DisplayMessage(message_type, Output.writeln_text(msg), show)) |
64642
c231206a84c8
display messages, according to regular Isabelle Output;
wenzelm
parents:
64605
diff
changeset
|
84 |
|
73340 | 85 |
def error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, true) |
86 |
def warning(msg: String): Unit = display_message(LSP.MessageType.Warning, msg, true) |
|
87 |
def writeln(msg: String): Unit = display_message(LSP.MessageType.Info, msg, true) |
|
64686 | 88 |
|
73340 | 89 |
def log_error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, false) |
90 |
def log_warning(msg: String): Unit = display_message(LSP.MessageType.Warning, msg, false) |
|
91 |
def log_writeln(msg: String): Unit = display_message(LSP.MessageType.Info, msg, false) |
|
64675 | 92 |
|
75393 | 93 |
object Error_Logger extends Logger { |
73340 | 94 |
def apply(msg: => String): Unit = log_error_message(msg) |
64810 | 95 |
} |
96 |
||
64675 | 97 |
|
64733 | 98 |
/* progress */ |
99 |
||
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
100 |
def progress(verbose: Boolean = false): Progress = { |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
101 |
val verbose_ = verbose |
64733 | 102 |
new Progress { |
77508 | 103 |
override val verbose: Boolean = verbose_ |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
104 |
override def echo(message: Progress.Message): Unit = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
105 |
message.kind match { |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
106 |
case Progress.Kind.writeln => log_writeln(message.text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
107 |
case Progress.Kind.warning => log_warning(message.text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
108 |
case Progress.Kind.error_message => log_error_message(message.text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
109 |
} |
64733 | 110 |
} |
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
111 |
} |
64605 | 112 |
} |