proper pattern matching for Notification0;
authorwenzelm
Mon, 27 Oct 2025 12:15:14 +0100
changeset 83415 e78d50e3e1eb
parent 83414 f61236e8c7b0
child 83416 c7849fa2ece0
proper pattern matching for Notification0;
src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 11:39:32 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Oct 27 12:15:14 2025 +0100
@@ -551,8 +551,8 @@
           case LSP.Documentation_Request => documentation_request()
           case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
             sledgehammer.handle_request(provers, isar, try0, purpose)
-          case LSP.Sledgehammer_Cancel => sledgehammer.cancel()
-          case LSP.Sledgehammer_Provers_Request => sledgehammer.send_provers()
+          case LSP.Sledgehammer_Cancel(()) => sledgehammer.cancel()
+          case LSP.Sledgehammer_Provers_Request(()) => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }