diff --git a/app/Main.hs b/app/Main.hs index d17d009..11f15e9 100644 --- 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 index 46c8570..5124db6 100644 --- 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