--- a/src/Tools/VSCode/src/lsp.scala Mon Oct 27 11:01:04 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala Mon Oct 27 11:09:41 2025 +0100
@@ -770,14 +770,8 @@
/* documentation */
- object Documentation_Request {
- def unapply(json: JSON.T): Option[Boolean] =
- json match {
- case Notification("PIDE/documentation_request", Some(params)) =>
- JSON.bool(params, "init")
- case _ => None
- }
- }
+ object Documentation_Request
+ extends Notification0("PIDE/documentation_request")
object Doc_Entry {
def apply(entry: Doc.Entry): JSON.T =