[ fix ] Place dummy handlers for initialized and `workspace/didChan…

…geConfiguration` to prevent the client from getting nasty errors
agda · Dec 4, 2024 · 38a7edd · 38a7edd
1 parent 79039ef
commit 38a7edd
Show file tree

Hide file tree

Showing 2 changed files with 68 additions and 77 deletions.
diff --git a/app/Main.hs b/app/Main.hs
@@ -3,6 +3,7 @@ module Main where
 import Control.Monad (when)
 import Options
 import Server (run)
+-- import Simple (run)
 import System.Console.GetOpt
 import System.Directory (doesDirectoryExist)
 import System.Environment
@@ -33,4 +34,5 @@ main = do
     then putStrLn usageMessage
     else do
       _ <- run options
+      -- _ <- run
       return ()
diff --git a/src/Server.hs b/src/Server.hs
@@ -2,45 +2,30 @@
 
 -- entry point of the LSP server
 
-module Server
-  ( run,
-  )
-where
+module Server (run) where
 
 import qualified Agda
-import           Control.Concurrent             ( writeChan )
-import           Control.Monad                  ( void )
-import           Control.Monad.Reader           ( MonadIO(liftIO) )
-import           Data.Aeson                     ( FromJSON
-                                                , ToJSON
-                                                )
-import qualified Data.Aeson                    as JSON
-import           Data.Text                      ( pack )
-import           GHC.IO.IOMode                  ( IOMode(ReadWriteMode) )
-import           Language.LSP.Server     hiding ( Options )
-import           Language.LSP.Protocol.Message  ( pattern RequestMessage
-                                                , SMethod( SMethod_CustomMethod, SMethod_TextDocumentHover)
-                                                , pattern TRequestMessage
-                                                )
-import           Language.LSP.Protocol.Types    ( TextDocumentSyncOptions(..)
-                                                , TextDocumentSyncKind( TextDocumentSyncKind_Incremental )
-                                                , ServerCapabilities (_textDocumentSync )
-                                                , SaveOptions( SaveOptions )
-                                                , pattern TextDocumentIdentifier
-                                                , pattern HoverParams
-                                                , pattern InR
-                                                , pattern InL
-                                                )
-import           Monad
-import qualified Network.Simple.TCP            as TCP
-import           Network.Socket                 ( socketToHandle )
+import Control.Concurrent (writeChan)
+import Control.Monad (void)
+import Control.Monad.Reader (MonadIO (liftIO))
+import Data.Aeson
+  ( FromJSON,
+    ToJSON,
+  )
+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.Server hiding (Options)
+import qualified Language.LSP.Server hiding (Options)
+import Monad
+import qualified Network.Simple.TCP as TCP
+import Network.Socket (socketToHandle)
+import Options
+import qualified Server.Handler as Handler
+import Switchboard (Switchboard, agdaCustomMethod)
 import qualified Switchboard
-import           Switchboard                    ( Switchboard, agdaCustomMethod )
-
-import qualified Server.Handler                as Handler
-
-import qualified Language.LSP.Server           as LSP
-import           Options
 
 --------------------------------------------------------------------------------
 
@@ -63,8 +48,7 @@ run options = do
     serverDefn :: Options -> ServerDefinition Config
     serverDefn options =
       ServerDefinition
-        { 
-          defaultConfig = initConfig,
+        { defaultConfig = initConfig,
           onConfigChange = const $ pure (),
           parseConfig = \old newRaw -> case JSON.fromJSON newRaw of
             JSON.Error s -> Left $ pack $ "Cannot parse server configuration: " <> s
@@ -77,52 +61,57 @@ run options = do
           configSection = "dummy",
           staticHandlers = const handlers,
           interpretHandler = \(ctxEnv, env) ->
-            Iso {
-              forward = runLspT ctxEnv . runServerM env,
-              backward = liftIO
-            },
-          options = lspOptions
+            Iso
+              { forward = runLspT ctxEnv . runServerM env,
+                backward = liftIO
+              },
+          options = defaultOptions
         }
 
-    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
-    syncOptions :: TextDocumentSyncOptions
-    syncOptions =
-      TextDocumentSyncOptions
-        { _openClose = Just True, -- receive open and close notifications from the client
-          _change = Just changeOptions, -- 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
-        }
+-- -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client
+-- syncOptions :: TextDocumentSyncOptions
+-- syncOptions =
+--   TextDocumentSyncOptions
+--     { _openClose = Just True, -- receive open and close notifications from the client
+--       _change = Just changeOptions, -- 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
+--     }
 
-    changeOptions :: TextDocumentSyncKind
-    changeOptions = TextDocumentSyncKind_Incremental
+-- 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)
+-- includes the document content on save, so that we don't have to read it from the disk
+-- saveOptions :: SaveOptions
+-- saveOptions = SaveOptions (Just True)
 
 -- handlers of the LSP server
 handlers :: Handlers (ServerM (LspM Config))
-handlers = mconcat
-  [ -- custom methods, not part of LSP
-    requestHandler agdaCustomMethod $ \ req responder -> do
-      let TRequestMessage _ _i _ params = req
-      response <- Agda.sendCommand params
-      responder $ Right response
-  ,
-        -- hover provider
-    requestHandler hoverMethod $ \ req responder -> do
-      let TRequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) = req
-      result <- Handler.onHover uri pos
-      responder $ Right result
-  -- -- syntax highlighting
-  -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do
-  --   result <- Handler.onHighlight (req ^. (params . textDocument . uri))
-  --   responder result
-  ]
+handlers =
+  mconcat
+    [ -- custom methods, not part of LSP
+      requestHandler agdaCustomMethod $ \req responder -> do
+        let TRequestMessage _ _i _ params = req
+        response <- Agda.sendCommand params
+        responder $ Right response,
+      -- hover provider
+      requestHandler hoverMethod $ \req responder -> do
+        let TRequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) = req
+        result <- Handler.onHover uri pos
+        responder $ Right result,
+      -- -- syntax highlighting
+      -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do
+      --   result <- Handler.onHighlight (req ^. (params . textDocument . uri))
+      --   responder result
+
+      -- must provide handler for `initialized` otherwise the client will get nasty error messages
+      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