clarified signature: proper 0-parameter pattern;

--- a/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 16:20:06 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Oct 29 13:26:26 2025 +0100
@@ -514,9 +514,9 @@
       try {
         json match {
           case LSP.Initialize(id) => init(id)
-          case LSP.Initialized(()) =>
+          case LSP.Initialized() =>
           case LSP.Shutdown(id) => shutdown(id)
-          case LSP.Exit(()) => exit()
+          case LSP.Exit() => exit()
           case LSP.DidOpenTextDocument(file, _, version, text) =>
             change_document(file, version, List(LSP.TextDocumentChange(None, text)))
             delay_load.invoke()
@@ -524,11 +524,11 @@
             change_document(file, version, changes)
           case LSP.DidCloseTextDocument(file) => close_document(file)
           case LSP.Completion(id, node_pos) => completion(id, node_pos)
-          case LSP.Include_Word(()) => update_dictionary(true, false)
-          case LSP.Include_Word_Permanently(()) => update_dictionary(true, true)
-          case LSP.Exclude_Word(()) => update_dictionary(false, false)
-          case LSP.Exclude_Word_Permanently(()) => update_dictionary(false, true)
-          case LSP.Reset_Words(()) => reset_dictionary()
+          case LSP.Include_Word() => update_dictionary(true, false)
+          case LSP.Include_Word_Permanently() => update_dictionary(true, true)
+          case LSP.Exclude_Word() => update_dictionary(false, false)
+          case LSP.Exclude_Word_Permanently() => update_dictionary(false, true)
+          case LSP.Reset_Words() => reset_dictionary()
           case LSP.Hover(id, node_pos) => hover(id, node_pos)
           case LSP.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
           case LSP.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
@@ -551,10 +551,10 @@
           case LSP.Documentation_Request => documentation_request()
           case LSP.Sledgehammer_Request(provers, isar, try0) =>
             sledgehammer.handle_request(provers, isar, try0)
-          case LSP.Sledgehammer_Cancel(()) => sledgehammer.cancel()
-          case LSP.Sledgehammer_Locate(()) => sledgehammer.locate()
-          case LSP.Sledgehammer_Insert(()) => sledgehammer.insert()
-          case LSP.Sledgehammer_Provers_Request(()) => sledgehammer.send_provers()
+          case LSP.Sledgehammer_Cancel() => sledgehammer.cancel()
+          case LSP.Sledgehammer_Locate() => sledgehammer.locate()
+          case LSP.Sledgehammer_Insert() => sledgehammer.insert()
+          case LSP.Sledgehammer_Provers_Request() => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }

--- a/src/Tools/VSCode/src/lsp.scala	Mon Oct 27 16:20:06 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Wed Oct 29 13:26:26 2025 +0100
@@ -47,10 +47,10 @@
   }
 
   class Notification0(name: String) {
-    def unapply(json: JSON.T): Option[Unit] =
+    def unapply(json: JSON.T): Boolean =
       json match {
-        case Notification(method, _) if method == name => Some(())
-        case _ => None
+        case Notification(method, _) => method == name
+        case _ => false
       }
   }