diff --git a/CHANGELOG.md b/CHANGELOG.md index 78542de..196d3a6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,11 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). +## v0.2.7.0.1.3 - 2024-12-5 + +### Fixed +- Add dummy LSP handlers for `initialized`, `workspace/didChangeConfiguration`, `textDocument/didOpen`, `textDocument/didClose`, `textDocument/didChange`, and `textDocument/didSave` to avoid errors in the client. + ## v0.2.7.0.1.2 - 2024-12-4 ### Fixed diff --git a/agda-language-server.cabal b/agda-language-server.cabal index f1b340b..e54db4a 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -5,7 +5,7 @@ cabal-version: 1.12 -- see: https://github.com/sol/hpack name: agda-language-server -version: 0.2.7.0.1.2 +version: 0.2.7.0.1.3 synopsis: An implementation of language server protocal (LSP) for Agda 2. description: Please see the README on GitHub at category: Development diff --git a/package.yaml b/package.yaml index 1706ec6..8b61ae5 100644 --- a/package.yaml +++ b/package.yaml @@ -1,5 +1,5 @@ name: agda-language-server -version: 0.2.7.0.1.2 +version: 0.2.7.0.1.3 github: "banacorn/agda-language-server" license: MIT author: "Ting-Gian LUA" diff --git a/src/Options.hs b/src/Options.hs index a63f34d..ee1fd5a 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -59,7 +59,7 @@ options = ] usage :: String -usage = "Agda v2.7.0.1 Language Server v2\nUsage: als [Options...]\n" +usage = "Agda v2.7.0.1 Language Server v3\nUsage: als [Options...]\n" usageAboutAgdaOptions :: String usageAboutAgdaOptions = diff --git a/src/Server.hs b/src/Server.hs index 5124db6..c9b1ffc 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -16,9 +16,10 @@ import qualified Data.Aeson as JSON import Data.Text (pack) import GHC.IO.IOMode (IOMode (ReadWriteMode)) import Language.LSP.Protocol.Message -import Language.LSP.Protocol.Types +import Language.LSP.Protocol.Types (HoverParams (..), SaveOptions (..), TextDocumentIdentifier (..), TextDocumentSyncKind (..), TextDocumentSyncOptions (..), type (|?) (..)) import Language.LSP.Server hiding (Options) import qualified Language.LSP.Server hiding (Options) +import qualified Language.LSP.Server as LSP import Monad import qualified Network.Simple.TCP as TCP import Network.Socket (socketToHandle) @@ -65,13 +66,13 @@ run options = do { forward = runLspT ctxEnv . runServerM env, backward = liftIO }, - options = defaultOptions + options = lspOptions } --- lspOptions :: LSP.Options --- lspOptions = defaultOptions { optTextDocumentSync = Just syncOptions } +lspOptions :: LSP.Options +lspOptions = defaultOptions {optTextDocumentSync = Just syncOptions} --- -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client +-- these `TextDocumentSyncOptions` are essential for receiving notifications from the client -- syncOptions :: TextDocumentSyncOptions -- syncOptions = -- TextDocumentSyncOptions @@ -81,13 +82,15 @@ run options = do -- _willSaveWaitUntil = Just False, -- receive willSave notifications from the client -- _save = Just $ InR saveOptions -- } - --- changeOptions :: TextDocumentSyncKind --- changeOptions = TextDocumentSyncKind_Incremental - --- includes the document content on save, so that we don't have to read it from the disk --- saveOptions :: SaveOptions --- saveOptions = SaveOptions (Just True) +syncOptions :: TextDocumentSyncOptions +syncOptions = + TextDocumentSyncOptions + { _openClose = Just True, -- receive open and close notifications from the client + _change = Just TextDocumentSyncKind_Incremental, -- receive change notifications from the client + _willSave = Just False, -- receive willSave notifications from the client + _willSaveWaitUntil = Just False, -- receive willSave notifications from the client + _save = Just $ InR $ SaveOptions (Just True) -- includes the document content on save, so that we don't have to read it from the disk (not sure if this is still true in lsp 2) + } -- handlers of the LSP server handlers :: Handlers (ServerM (LspM Config)) @@ -98,8 +101,8 @@ handlers = let TRequestMessage _ _i _ params = req response <- Agda.sendCommand params responder $ Right response, - -- hover provider - requestHandler hoverMethod $ \req responder -> do + -- `textDocument/hover` + requestHandler SMethod_TextDocumentHover $ \req responder -> do let TRequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) = req result <- Handler.onHover uri pos responder $ Right result, @@ -108,10 +111,16 @@ handlers = -- result <- Handler.onHighlight (req ^. (params . textDocument . uri)) -- responder result - -- must provide handler for `initialized` otherwise the client will get nasty error messages + -- `initialized` notificationHandler SMethod_Initialized $ \_notification -> return (), - -- must provide handler for `workspace/didChangeConfiguration` otherwise the client will get nasty error messages - notificationHandler SMethod_WorkspaceDidChangeConfiguration $ \_notification -> return () - ] - where - hoverMethod = SMethod_TextDocumentHover + -- `workspace/didChangeConfiguration` + notificationHandler SMethod_WorkspaceDidChangeConfiguration $ \_notification -> return (), + -- `textDocument/didOpen` + notificationHandler SMethod_TextDocumentDidOpen $ \_notification -> return (), + -- `textDocument/didClose` + notificationHandler SMethod_TextDocumentDidClose $ \_notification -> return (), + -- `textDocument/didChange` + notificationHandler SMethod_TextDocumentDidChange $ \_notification -> return (), + -- `textDocument/didSave` + notificationHandler SMethod_TextDocumentDidSave $ \_notification -> return () + ] \ No newline at end of file