1 /* Title: Tools/VSCode/src/protocol.scala |
|
2 Author: Makarius |
|
3 |
|
4 Message formats for Language Server Protocol 3.0, see |
|
5 https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md |
|
6 */ |
|
7 |
|
8 package isabelle.vscode |
|
9 |
|
10 |
|
11 import isabelle._ |
|
12 |
|
13 import java.io.{File => JFile} |
|
14 |
|
15 |
|
16 object Protocol |
|
17 { |
|
18 /* abstract message */ |
|
19 |
|
20 object Message |
|
21 { |
|
22 val empty: JSON.Object.T = JSON.Object("jsonrpc" -> "2.0") |
|
23 |
|
24 def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean) |
|
25 { |
|
26 val header = |
|
27 json match { |
|
28 case JSON.Object(obj) => obj -- (obj.keySet - "method" - "id") |
|
29 case _ => JSON.Object.empty |
|
30 } |
|
31 if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json)) |
|
32 else logger(prefix + " " + JSON.Format(header)) |
|
33 } |
|
34 } |
|
35 |
|
36 |
|
37 /* notification */ |
|
38 |
|
39 object Notification |
|
40 { |
|
41 def apply(method: String, params: JSON.T): JSON.T = |
|
42 Message.empty + ("method" -> method) + ("params" -> params) |
|
43 |
|
44 def unapply(json: JSON.T): Option[(String, Option[JSON.T])] = |
|
45 for { |
|
46 method <- JSON.string(json, "method") |
|
47 params = JSON.value(json, "params") |
|
48 } yield (method, params) |
|
49 } |
|
50 |
|
51 class Notification0(name: String) |
|
52 { |
|
53 def unapply(json: JSON.T): Option[Unit] = |
|
54 json match { |
|
55 case Notification(method, _) if method == name => Some(()) |
|
56 case _ => None |
|
57 } |
|
58 } |
|
59 |
|
60 |
|
61 /* request message */ |
|
62 |
|
63 object Id |
|
64 { |
|
65 def empty: Id = Id("") |
|
66 } |
|
67 |
|
68 sealed case class Id(id: Any) |
|
69 { |
|
70 require( |
|
71 id.isInstanceOf[Int] || |
|
72 id.isInstanceOf[Long] || |
|
73 id.isInstanceOf[Double] || |
|
74 id.isInstanceOf[String]) |
|
75 |
|
76 override def toString: String = id.toString |
|
77 } |
|
78 |
|
79 object RequestMessage |
|
80 { |
|
81 def apply(id: Id, method: String, params: JSON.T): JSON.T = |
|
82 Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params) |
|
83 |
|
84 def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] = |
|
85 for { |
|
86 id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id") |
|
87 method <- JSON.string(json, "method") |
|
88 params = JSON.value(json, "params") |
|
89 } yield (Id(id), method, params) |
|
90 } |
|
91 |
|
92 class Request0(name: String) |
|
93 { |
|
94 def unapply(json: JSON.T): Option[Id] = |
|
95 json match { |
|
96 case RequestMessage(id, method, _) if method == name => Some(id) |
|
97 case _ => None |
|
98 } |
|
99 } |
|
100 |
|
101 class RequestTextDocumentPosition(name: String) |
|
102 { |
|
103 def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] = |
|
104 json match { |
|
105 case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name => |
|
106 Some((id, node_pos)) |
|
107 case _ => None |
|
108 } |
|
109 } |
|
110 |
|
111 |
|
112 /* response message */ |
|
113 |
|
114 object ResponseMessage |
|
115 { |
|
116 def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T = |
|
117 Message.empty + ("id" -> id.id) ++ |
|
118 JSON.optional("result" -> result) ++ |
|
119 JSON.optional("error" -> error.map(_.json)) |
|
120 |
|
121 def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T = |
|
122 if (error == "") apply(id, result = result) |
|
123 else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error))) |
|
124 |
|
125 def is_empty(json: JSON.T): Boolean = |
|
126 JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined |
|
127 } |
|
128 |
|
129 sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None) |
|
130 { |
|
131 def json: JSON.T = |
|
132 JSON.Object("code" -> code, "message" -> message) ++ JSON.optional("data" -> data) |
|
133 } |
|
134 |
|
135 object ErrorCodes |
|
136 { |
|
137 val ParseError = -32700 |
|
138 val InvalidRequest = -32600 |
|
139 val MethodNotFound = -32601 |
|
140 val InvalidParams = -32602 |
|
141 val InternalError = -32603 |
|
142 val serverErrorStart = -32099 |
|
143 val serverErrorEnd = -32000 |
|
144 } |
|
145 |
|
146 |
|
147 /* init and exit */ |
|
148 |
|
149 object Initialize extends Request0("initialize") |
|
150 { |
|
151 def reply(id: Id, error: String): JSON.T = |
|
152 ResponseMessage.strict( |
|
153 id, Some(JSON.Object("capabilities" -> ServerCapabilities.json)), error) |
|
154 } |
|
155 |
|
156 object ServerCapabilities |
|
157 { |
|
158 val json: JSON.T = |
|
159 JSON.Object( |
|
160 "textDocumentSync" -> 2, |
|
161 "completionProvider" -> JSON.Object("resolveProvider" -> false, "triggerCharacters" -> Nil), |
|
162 "hoverProvider" -> true, |
|
163 "definitionProvider" -> true, |
|
164 "documentHighlightProvider" -> true) |
|
165 } |
|
166 |
|
167 object Initialized extends Notification0("initialized") |
|
168 |
|
169 object Shutdown extends Request0("shutdown") |
|
170 { |
|
171 def reply(id: Id, error: String): JSON.T = |
|
172 ResponseMessage.strict(id, Some("OK"), error) |
|
173 } |
|
174 |
|
175 object Exit extends Notification0("exit") |
|
176 |
|
177 |
|
178 /* document positions */ |
|
179 |
|
180 object Position |
|
181 { |
|
182 def apply(pos: Line.Position): JSON.T = |
|
183 JSON.Object("line" -> pos.line, "character" -> pos.column) |
|
184 |
|
185 def unapply(json: JSON.T): Option[Line.Position] = |
|
186 for { |
|
187 line <- JSON.int(json, "line") |
|
188 column <- JSON.int(json, "character") |
|
189 } yield Line.Position(line, column) |
|
190 } |
|
191 |
|
192 object Range |
|
193 { |
|
194 def compact(range: Line.Range): List[Int] = |
|
195 List(range.start.line, range.start.column, range.stop.line, range.stop.column) |
|
196 |
|
197 def apply(range: Line.Range): JSON.T = |
|
198 JSON.Object("start" -> Position(range.start), "end" -> Position(range.stop)) |
|
199 |
|
200 def unapply(json: JSON.T): Option[Line.Range] = |
|
201 (JSON.value(json, "start"), JSON.value(json, "end")) match { |
|
202 case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop)) |
|
203 case _ => None |
|
204 } |
|
205 } |
|
206 |
|
207 object Location |
|
208 { |
|
209 def apply(loc: Line.Node_Range): JSON.T = |
|
210 JSON.Object("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range)) |
|
211 |
|
212 def unapply(json: JSON.T): Option[Line.Node_Range] = |
|
213 for { |
|
214 uri <- JSON.string(json, "uri") |
|
215 range_json <- JSON.value(json, "range") |
|
216 range <- Range.unapply(range_json) |
|
217 } yield Line.Node_Range(Url.absolute_file_name(uri), range) |
|
218 } |
|
219 |
|
220 object TextDocumentPosition |
|
221 { |
|
222 def unapply(json: JSON.T): Option[Line.Node_Position] = |
|
223 for { |
|
224 doc <- JSON.value(json, "textDocument") |
|
225 uri <- JSON.string(doc, "uri") |
|
226 pos_json <- JSON.value(json, "position") |
|
227 pos <- Position.unapply(pos_json) |
|
228 } yield Line.Node_Position(Url.absolute_file_name(uri), pos) |
|
229 } |
|
230 |
|
231 |
|
232 /* marked strings */ |
|
233 |
|
234 sealed case class MarkedString(text: String, language: String = "plaintext") |
|
235 { |
|
236 def json: JSON.T = JSON.Object("language" -> language, "value" -> text) |
|
237 } |
|
238 |
|
239 object MarkedStrings |
|
240 { |
|
241 def json(msgs: List[MarkedString]): Option[JSON.T] = |
|
242 msgs match { |
|
243 case Nil => None |
|
244 case List(msg) => Some(msg.json) |
|
245 case _ => Some(msgs.map(_.json)) |
|
246 } |
|
247 } |
|
248 |
|
249 |
|
250 /* diagnostic messages */ |
|
251 |
|
252 object MessageType |
|
253 { |
|
254 val Error = 1 |
|
255 val Warning = 2 |
|
256 val Info = 3 |
|
257 val Log = 4 |
|
258 } |
|
259 |
|
260 object DisplayMessage |
|
261 { |
|
262 def apply(message_type: Int, message: String, show: Boolean = true): JSON.T = |
|
263 Notification(if (show) "window/showMessage" else "window/logMessage", |
|
264 JSON.Object("type" -> message_type, "message" -> message)) |
|
265 } |
|
266 |
|
267 |
|
268 /* commands */ |
|
269 |
|
270 sealed case class Command(title: String, command: String, arguments: List[JSON.T] = Nil) |
|
271 { |
|
272 def json: JSON.T = |
|
273 JSON.Object("title" -> title, "command" -> command, "arguments" -> arguments) |
|
274 } |
|
275 |
|
276 |
|
277 /* document edits */ |
|
278 |
|
279 object DidOpenTextDocument |
|
280 { |
|
281 def unapply(json: JSON.T): Option[(JFile, String, Long, String)] = |
|
282 json match { |
|
283 case Notification("textDocument/didOpen", Some(params)) => |
|
284 for { |
|
285 doc <- JSON.value(params, "textDocument") |
|
286 uri <- JSON.string(doc, "uri") |
|
287 lang <- JSON.string(doc, "languageId") |
|
288 version <- JSON.long(doc, "version") |
|
289 text <- JSON.string(doc, "text") |
|
290 } yield (Url.absolute_file(uri), lang, version, text) |
|
291 case _ => None |
|
292 } |
|
293 } |
|
294 |
|
295 |
|
296 sealed case class TextDocumentChange(range: Option[Line.Range], text: String) |
|
297 |
|
298 object DidChangeTextDocument |
|
299 { |
|
300 def unapply_change(json: JSON.T): Option[TextDocumentChange] = |
|
301 for { text <- JSON.string(json, "text") } |
|
302 yield TextDocumentChange(JSON.value(json, "range", Range.unapply _), text) |
|
303 |
|
304 def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentChange])] = |
|
305 json match { |
|
306 case Notification("textDocument/didChange", Some(params)) => |
|
307 for { |
|
308 doc <- JSON.value(params, "textDocument") |
|
309 uri <- JSON.string(doc, "uri") |
|
310 version <- JSON.long(doc, "version") |
|
311 changes <- JSON.list(params, "contentChanges", unapply_change _) |
|
312 } yield (Url.absolute_file(uri), version, changes) |
|
313 case _ => None |
|
314 } |
|
315 } |
|
316 |
|
317 class TextDocumentNotification(name: String) |
|
318 { |
|
319 def unapply(json: JSON.T): Option[JFile] = |
|
320 json match { |
|
321 case Notification(method, Some(params)) if method == name => |
|
322 for { |
|
323 doc <- JSON.value(params, "textDocument") |
|
324 uri <- JSON.string(doc, "uri") |
|
325 } yield Url.absolute_file(uri) |
|
326 case _ => None |
|
327 } |
|
328 } |
|
329 |
|
330 object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose") |
|
331 object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave") |
|
332 |
|
333 |
|
334 /* workspace edits */ |
|
335 |
|
336 sealed case class TextEdit(range: Line.Range, new_text: String) |
|
337 { |
|
338 def json: JSON.T = JSON.Object("range" -> Range(range), "newText" -> new_text) |
|
339 } |
|
340 |
|
341 sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit]) |
|
342 { |
|
343 def json: JSON.T = |
|
344 JSON.Object( |
|
345 "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version), |
|
346 "edits" -> edits.map(_.json)) |
|
347 } |
|
348 |
|
349 object WorkspaceEdit |
|
350 { |
|
351 def apply(edits: List[TextDocumentEdit]): JSON.T = |
|
352 RequestMessage(Id.empty, "workspace/applyEdit", |
|
353 JSON.Object("edit" -> JSON.Object("documentChanges" -> edits.map(_.json)))) |
|
354 } |
|
355 |
|
356 |
|
357 /* completion */ |
|
358 |
|
359 sealed case class CompletionItem( |
|
360 label: String, |
|
361 kind: Option[Int] = None, |
|
362 detail: Option[String] = None, |
|
363 documentation: Option[String] = None, |
|
364 text: Option[String] = None, |
|
365 range: Option[Line.Range] = None, |
|
366 command: Option[Command] = None) |
|
367 { |
|
368 def json: JSON.T = |
|
369 JSON.Object("label" -> label) ++ |
|
370 JSON.optional("kind" -> kind) ++ |
|
371 JSON.optional("detail" -> detail) ++ |
|
372 JSON.optional("documentation" -> documentation) ++ |
|
373 JSON.optional("insertText" -> text) ++ |
|
374 JSON.optional("range" -> range.map(Range(_))) ++ |
|
375 JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++ |
|
376 JSON.optional("command" -> command.map(_.json)) |
|
377 } |
|
378 |
|
379 object Completion extends RequestTextDocumentPosition("textDocument/completion") |
|
380 { |
|
381 def reply(id: Id, result: List[CompletionItem]): JSON.T = |
|
382 ResponseMessage(id, Some(result.map(_.json))) |
|
383 } |
|
384 |
|
385 |
|
386 /* spell checker */ |
|
387 |
|
388 object Include_Word extends Notification0("PIDE/include_word") |
|
389 { |
|
390 val command = Command("Include word", "isabelle.include-word") |
|
391 } |
|
392 |
|
393 object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently") |
|
394 { |
|
395 val command = Command("Include word permanently", "isabelle.include-word-permanently") |
|
396 } |
|
397 |
|
398 object Exclude_Word extends Notification0("PIDE/exclude_word") |
|
399 { |
|
400 val command = Command("Exclude word", "isabelle.exclude-word") |
|
401 } |
|
402 |
|
403 object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently") |
|
404 { |
|
405 val command = Command("Exclude word permanently", "isabelle.exclude-word-permanently") |
|
406 } |
|
407 |
|
408 object Reset_Words extends Notification0("PIDE/reset_words") |
|
409 { |
|
410 val command = Command("Reset non-permanent words", "isabelle.reset-words") |
|
411 } |
|
412 |
|
413 |
|
414 /* hover request */ |
|
415 |
|
416 object Hover extends RequestTextDocumentPosition("textDocument/hover") |
|
417 { |
|
418 def reply(id: Id, result: Option[(Line.Range, List[MarkedString])]): JSON.T = |
|
419 { |
|
420 val res = |
|
421 result match { |
|
422 case Some((range, contents)) => |
|
423 JSON.Object( |
|
424 "contents" -> MarkedStrings.json(contents).getOrElse(Nil), |
|
425 "range" -> Range(range)) |
|
426 case None => JSON.Object("contents" -> Nil) |
|
427 } |
|
428 ResponseMessage(id, Some(res)) |
|
429 } |
|
430 } |
|
431 |
|
432 |
|
433 /* goto definition request */ |
|
434 |
|
435 object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition") |
|
436 { |
|
437 def reply(id: Id, result: List[Line.Node_Range]): JSON.T = |
|
438 ResponseMessage(id, Some(result.map(Location.apply(_)))) |
|
439 } |
|
440 |
|
441 |
|
442 /* document highlights request */ |
|
443 |
|
444 object DocumentHighlight |
|
445 { |
|
446 def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1)) |
|
447 def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2)) |
|
448 def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3)) |
|
449 } |
|
450 |
|
451 sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None) |
|
452 { |
|
453 def json: JSON.T = |
|
454 kind match { |
|
455 case None => JSON.Object("range" -> Range(range)) |
|
456 case Some(k) => JSON.Object("range" -> Range(range), "kind" -> k) |
|
457 } |
|
458 } |
|
459 |
|
460 object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight") |
|
461 { |
|
462 def reply(id: Id, result: List[DocumentHighlight]): JSON.T = |
|
463 ResponseMessage(id, Some(result.map(_.json))) |
|
464 } |
|
465 |
|
466 |
|
467 /* diagnostics */ |
|
468 |
|
469 sealed case class Diagnostic(range: Line.Range, message: String, |
|
470 severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None) |
|
471 { |
|
472 def json: JSON.T = |
|
473 Message.empty + ("range" -> Range(range)) + ("message" -> message) ++ |
|
474 JSON.optional("severity" -> severity) ++ |
|
475 JSON.optional("code" -> code) ++ |
|
476 JSON.optional("source" -> source) |
|
477 } |
|
478 |
|
479 object DiagnosticSeverity |
|
480 { |
|
481 val Error = 1 |
|
482 val Warning = 2 |
|
483 val Information = 3 |
|
484 val Hint = 4 |
|
485 } |
|
486 |
|
487 object PublishDiagnostics |
|
488 { |
|
489 def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T = |
|
490 Notification("textDocument/publishDiagnostics", |
|
491 JSON.Object("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json))) |
|
492 } |
|
493 |
|
494 |
|
495 /* decorations */ |
|
496 |
|
497 sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString]) |
|
498 { |
|
499 def json: JSON.T = |
|
500 JSON.Object("range" -> Range.compact(range)) ++ |
|
501 JSON.optional("hover_message" -> MarkedStrings.json(hover_message)) |
|
502 } |
|
503 |
|
504 sealed case class Decoration(typ: String, content: List[DecorationOpts]) |
|
505 { |
|
506 def json(file: JFile): JSON.T = |
|
507 Notification("PIDE/decoration", |
|
508 JSON.Object("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json))) |
|
509 } |
|
510 |
|
511 |
|
512 /* caret update: bidirectional */ |
|
513 |
|
514 object Caret_Update |
|
515 { |
|
516 def apply(node_pos: Line.Node_Position, focus: Boolean): JSON.T = |
|
517 Notification("PIDE/caret_update", |
|
518 JSON.Object( |
|
519 "uri" -> Url.print_file_name(node_pos.name), |
|
520 "line" -> node_pos.pos.line, |
|
521 "character" -> node_pos.pos.column, |
|
522 "focus" -> focus)) |
|
523 |
|
524 def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] = |
|
525 json match { |
|
526 case Notification("PIDE/caret_update", Some(params)) => |
|
527 val caret = |
|
528 for { |
|
529 uri <- JSON.string(params, "uri") |
|
530 if Url.is_wellformed_file(uri) |
|
531 pos <- Position.unapply(params) |
|
532 } yield (Url.absolute_file(uri), pos) |
|
533 Some(caret) |
|
534 case _ => None |
|
535 } |
|
536 } |
|
537 |
|
538 |
|
539 /* dynamic output */ |
|
540 |
|
541 object Dynamic_Output |
|
542 { |
|
543 def apply(content: String): JSON.T = |
|
544 Notification("PIDE/dynamic_output", JSON.Object("content" -> content)) |
|
545 } |
|
546 |
|
547 |
|
548 /* state output */ |
|
549 |
|
550 object State_Output |
|
551 { |
|
552 def apply(id: Counter.ID, content: String): JSON.T = |
|
553 Notification("PIDE/state_output", JSON.Object("id" -> id, "content" -> content)) |
|
554 } |
|
555 |
|
556 class State_Id_Notification(name: String) |
|
557 { |
|
558 def unapply(json: JSON.T): Option[Counter.ID] = |
|
559 json match { |
|
560 case Notification(method, Some(params)) if method == name => JSON.long(params, "id") |
|
561 case _ => None |
|
562 } |
|
563 } |
|
564 |
|
565 object State_Init extends Notification0("PIDE/state_init") |
|
566 object State_Exit extends State_Id_Notification("PIDE/state_exit") |
|
567 object State_Locate extends State_Id_Notification("PIDE/state_locate") |
|
568 object State_Update extends State_Id_Notification("PIDE/state_update") |
|
569 |
|
570 object State_Auto_Update |
|
571 { |
|
572 def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] = |
|
573 json match { |
|
574 case Notification("PIDE/state_auto_update", Some(params)) => |
|
575 for { |
|
576 id <- JSON.long(params, "id") |
|
577 enabled <- JSON.bool(params, "enabled") |
|
578 } yield (id, enabled) |
|
579 case _ => None |
|
580 } |
|
581 } |
|
582 |
|
583 |
|
584 /* preview */ |
|
585 |
|
586 object Preview_Request |
|
587 { |
|
588 def unapply(json: JSON.T): Option[(JFile, Int)] = |
|
589 json match { |
|
590 case Notification("PIDE/preview_request", Some(params)) => |
|
591 for { |
|
592 uri <- JSON.string(params, "uri") |
|
593 if Url.is_wellformed_file(uri) |
|
594 column <- JSON.int(params, "column") |
|
595 } yield (Url.absolute_file(uri), column) |
|
596 case _ => None |
|
597 } |
|
598 } |
|
599 |
|
600 object Preview_Response |
|
601 { |
|
602 def apply(file: JFile, column: Int, label: String, content: String): JSON.T = |
|
603 Notification("PIDE/preview_response", |
|
604 JSON.Object( |
|
605 "uri" -> Url.print_file(file), |
|
606 "column" -> column, |
|
607 "label" -> label, |
|
608 "content" -> content)) |
|
609 } |
|
610 |
|
611 |
|
612 /* Isabelle symbols */ |
|
613 |
|
614 object Symbols_Request extends Notification0("PIDE/symbols_request") |
|
615 |
|
616 object Symbols |
|
617 { |
|
618 def apply(): JSON.T = |
|
619 { |
|
620 val entries = |
|
621 for ((sym, code) <- Symbol.codes) |
|
622 yield JSON.Object("symbol" -> sym, "name" -> Symbol.names(sym)._1, "code" -> code) |
|
623 Notification("PIDE/symbols", JSON.Object("entries" -> entries)) |
|
624 } |
|
625 } |
|
626 } |
|