# HG changeset patch
# User wenzelm
# Date 1761559781 -3600
# Node ID 068cfdd057d087783a8f1efa8ef7921be003f9cf
# Parent  b1a472adb667bd39d7b8d71ed14e5610035399b8
discontinue pointless "init" flag;

diff -r b1a472adb667 -r 068cfdd057d0 src/Tools/VSCode/src/lsp.scala
--- 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 =