Skip to content

Commit a4b12c2

Browse files
nvarnernvarner
committed
refactor handlers, handle errors
1 parent 3707390 commit a4b12c2

File tree

7 files changed

+124
-51
lines changed

7 files changed

+124
-51
lines changed

‎agda-language-server.cabal‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,7 @@ library
8484
Server.Model
8585
Server.Model.AgdaFile
8686
Server.Model.AgdaLib
87+
Server.Model.Handler
8788
Server.Model.Monad
8889
Server.Model.Symbol
8990
Server.ResponseController
@@ -230,6 +231,7 @@ test-suite als-test
230231
Server.Model
231232
Server.Model.AgdaFile
232233
Server.Model.AgdaLib
234+
Server.Model.Handler
233235
Server.Model.Monad
234236
Server.Model.Symbol
235237
Server.ResponseController

‎src/Monad.hs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,11 @@ import Agda.Interaction.Base (IOTCM)
99
import Agda.Interaction.Library (findProjectRoot)
1010
import Agda.Interaction.Library.More (tryRunLibM)
1111
import Agda.TypeChecking.Monad (TCMT)
12+
import qualified Agda.TypeChecking.Monad as TCM
1213
import Agda.Utils.Lens (Lens', (^.))
1314
import Control.Concurrent
15+
import Control.Exception (Exception)
16+
import qualified Control.Exception as E
1417
import Control.Monad.Reader
1518
import Data.IORef
1619
( IORef,
@@ -30,6 +33,7 @@ import Language.LSP.Server
3033
MonadLsp,
3134
getConfig,
3235
)
36+
import qualified Language.LSP.Server as LSP
3337
import Options
3438
import Server.CommandController (CommandController)
3539
import qualified Server.CommandController as CommandController
@@ -113,6 +117,12 @@ findAgdaLib uri = do
113117
modifyModel $ Model.withAgdaLib lib
114118
return lib
115119

120+
catchTCError :: ServerM a -> (TCM.TCErr -> ServerM a) -> ServerM a
121+
catchTCError m h =
122+
ReaderT $ \env -> LSP.LspT $ ReaderT $ \lspEnv ->
123+
LSP.runLspT lspEnv (runServerT env m)
124+
`E.catch` \err -> LSP.runLspT lspEnv (runServerT env (h err))
125+
116126
-- | Provider
117127
provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerT m ()
118128
provideCommand iotcm = do

‎src/Server/Handler/TextDocument/DocumentSymbol.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ import qualified Language.LSP.Protocol.Types as LSP
1313
import qualified Language.LSP.Server as LSP
1414
import Monad (ServerM)
1515
import Server.Model.AgdaFile (AgdaFile, agdaFileSymbols, defNameRange, symbolByName, symbolsByParent)
16-
import Server.Model.Monad (MonadAgdaFile (askAgdaFile), requestHandlerWithAgdaFile, useAgdaFile)
16+
import Server.Model.Handler (requestHandlerWithAgdaFile)
17+
import Server.Model.Monad (MonadAgdaFile (askAgdaFile), useAgdaFile)
1718
import Server.Model.Symbol (SymbolInfo (symbolName), lspSymbolKind, symbolShortName, symbolType)
1819

1920
documentSymbolHandler :: LSP.Handlers ServerM

‎src/Server/Handler/TextDocument/FileManagement.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,22 +20,22 @@ import qualified Language.LSP.Server as VFS
2020
import qualified Language.LSP.VFS as VFS
2121
import Monad (ServerM, modifyModel)
2222
import qualified Server.Model as Model
23-
import Server.Model.Monad (notificationHandlerWithAgdaLib)
23+
import Server.Model.Handler (notificationHandlerWithAgdaLib)
2424

2525
didOpenHandler :: LSP.Handlers ServerM
26-
didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen $ \notification uri -> do
26+
didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen $ \uri notification -> do
2727
sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri
2828
let sourceText = toLazy $ notification ^. LSP.params . LSP.textDocument . LSP.text
2929
src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText
3030
agdaFile <- indexFile src
3131
lift $ modifyModel $ Model.setAgdaFile uri agdaFile
3232

3333
didCloseHandler :: LSP.Handlers ServerM
34-
didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClose $ \notification uri -> do
34+
didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClose $ \uri notification -> do
3535
lift $ modifyModel $ Model.deleteAgdaFile uri
3636

3737
didSaveHandler :: LSP.Handlers ServerM
38-
didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \notification uri -> do
38+
didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \uri notification -> do
3939
sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri
4040
virtualFile <- lift $ VFS.getVirtualFile uri
4141
case virtualFile of

‎src/Server/Model/Handler.hs‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE FlexibleContexts #-}
3+
{-# LANGUAGE KindSignatures #-}
4+
{-# LANGUAGE PolyKinds #-}
5+
{-# LANGUAGE RankNTypes #-}
6+
7+
module Server.Model.Handler
8+
( notificationHandlerWithAgdaLib,
9+
requestHandlerWithAgdaFile,
10+
)
11+
where
12+
13+
import Agda.Syntax.Common (WithHiding (whHiding))
14+
import Agda.Syntax.Common.Pretty (prettyShow)
15+
import qualified Agda.TypeChecking.Monad as TCM
16+
import qualified Agda.TypeChecking.Pretty as TCM
17+
import Agda.Utils.Either (fromRightM)
18+
import Agda.Utils.Lens ((^.))
19+
import Control.Monad.Trans (MonadTrans, lift)
20+
import qualified Data.Text as Text
21+
import qualified Language.LSP.Protocol.Lens as LSP
22+
import qualified Language.LSP.Protocol.Message as LSP
23+
import qualified Language.LSP.Protocol.Message as Lsp
24+
import qualified Language.LSP.Protocol.Types as LSP
25+
import qualified Language.LSP.Server as LSP
26+
import Monad (ServerM, askModel, catchTCError, findAgdaLib)
27+
import qualified Server.Model as Model
28+
import Server.Model.Monad (WithAgdaFileM, WithAgdaLibM, runWithAgdaFileT, runWithAgdaLibT)
29+
30+
tryTC :: ServerM a -> ServerM (Either TCM.TCErr a)
31+
tryTC handler = (Right <$> handler) `catchTCError` (return . Left)
32+
33+
--------------------------------------------------------------------------------
34+
35+
type NotificationHandlerWithAgdaLib
36+
(m :: LSP.Method LSP.ClientToServer LSP.Notification) =
37+
LSP.NormalizedUri -> LSP.TNotificationMessage m -> WithAgdaLibM ()
38+
39+
notificationHandlerWithAgdaLib ::
40+
(LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) =>
41+
LSP.SMethod m ->
42+
NotificationHandlerWithAgdaLib m ->
43+
LSP.Handlers ServerM
44+
notificationHandlerWithAgdaLib m handlerWithAgdaLib = LSP.notificationHandler m $ \notification -> do
45+
let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri
46+
normUri = LSP.toNormalizedUri uri
47+
agdaLib <- findAgdaLib normUri
48+
49+
let notificationHandler = runWithAgdaLibT agdaLib . handlerWithAgdaLib normUri
50+
let handler = tryTC $ notificationHandler notification
51+
52+
let onErr = \err -> runWithAgdaLibT agdaLib $ do
53+
message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err)
54+
lift $ LSP.sendNotification LSP.SMethod_WindowShowMessage $ LSP.ShowMessageParams LSP.MessageType_Error message
55+
56+
fromRightM onErr handler
57+
58+
--------------------------------------------------------------------------------
59+
60+
type RequestCallbackWithAgdaFile
61+
(m :: LSP.Method LSP.ClientToServer LSP.Request) =
62+
Either (LSP.TResponseError m) (LSP.MessageResult m) -> WithAgdaFileM ()
63+
64+
type RequestHandlerWithAgdaFile
65+
(m :: LSP.Method LSP.ClientToServer LSP.Request) =
66+
LSP.TRequestMessage m ->
67+
RequestCallbackWithAgdaFile m ->
68+
WithAgdaFileM ()
69+
70+
requestHandlerWithAgdaFile ::
71+
(LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) =>
72+
LSP.SMethod m ->
73+
RequestHandlerWithAgdaFile m ->
74+
LSP.Handlers ServerM
75+
requestHandlerWithAgdaFile m handlerWithAgdaFile = LSP.requestHandler m $ \req responder -> do
76+
let uri = req ^. LSP.params . LSP.textDocument . LSP.uri
77+
normUri = LSP.toNormalizedUri uri
78+
79+
model <- askModel
80+
case Model.getAgdaFile normUri model of
81+
Nothing -> do
82+
let message = "Request for unknown Agda file at URI: " <> LSP.getUri uri
83+
responder $ Left $ LSP.TResponseError (LSP.InR LSP.ErrorCodes_InvalidParams) message Nothing
84+
Just agdaFile -> do
85+
agdaLib <- Model.getAgdaLib normUri model
86+
let responderWithAgdaFile = lift . responder
87+
let handler = tryTC $ runWithAgdaFileT agdaLib agdaFile $ handlerWithAgdaFile req responderWithAgdaFile
88+
89+
let onErr = \err -> runWithAgdaFileT agdaLib agdaFile $ do
90+
message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err)
91+
lift $ responder $ Left $ LSP.TResponseError (LSP.InL LSP.LSPErrorCodes_RequestFailed) message Nothing
92+
93+
fromRightM onErr handler

‎src/Server/Model/Monad.hs‎

Lines changed: 11 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -10,30 +10,37 @@
1010
module Server.Model.Monad
1111
( MonadAgdaLib (..),
1212
useAgdaLib,
13-
notificationHandlerWithAgdaLib,
1413
MonadAgdaFile (..),
1514
useAgdaFile,
16-
requestHandlerWithAgdaFile,
15+
WithAgdaLibT,
16+
runWithAgdaLibT,
1717
WithAgdaLibM,
1818
runWithAgdaLib,
19+
WithAgdaFileT,
20+
runWithAgdaFileT,
21+
WithAgdaFileM,
1922
)
2023
where
2124

2225
import Agda.Interaction.Options (CommandLineOptions (optPragmaOptions), PragmaOptions)
23-
import Agda.TypeChecking.Monad (HasOptions (..), MonadTCEnv (..), MonadTCM (..), MonadTCState (..), PersistentTCState (stPersistentOptions), ReadTCState (..), TCEnv, TCM, TCMT (..), TCState (stPersistentState), modifyTCLens, setTCLens, stPragmaOptions, useTC)
26+
import Agda.Syntax.Common.Pretty (prettyShow)
27+
import Agda.TypeChecking.Monad (HasOptions (..), MonadTCEnv (..), MonadTCM (..), MonadTCState (..), PersistentTCState (stPersistentOptions), ReadTCState (..), TCEnv, TCM, TCMT (..), TCState (stPersistentState), catchError_, modifyTCLens, setTCLens, stPragmaOptions, useTC)
28+
import qualified Agda.TypeChecking.Monad as TCM
29+
import qualified Agda.TypeChecking.Pretty as TCM
2430
import Agda.Utils.IORef (modifyIORef', readIORef, writeIORef)
2531
import Agda.Utils.Lens (Lens', locally, over, use, view, (<&>), (^.))
2632
import Agda.Utils.Monad (bracket_)
2733
import Control.Monad.IO.Class (MonadIO (liftIO))
2834
import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), ask, asks)
2935
import Control.Monad.Trans (MonadTrans, lift)
36+
import qualified Data.Text as Text
3037
import qualified Language.LSP.Protocol.Lens as LSP
3138
import qualified Language.LSP.Protocol.Message as LSP
3239
import qualified Language.LSP.Protocol.Types as LSP
3340
import qualified Language.LSP.Protocol.Types.Uri.More as LSP
3441
import Language.LSP.Server (LspM)
3542
import qualified Language.LSP.Server as LSP
36-
import Monad (ServerM, ServerT, askModel, findAgdaLib)
43+
import Monad (ServerM, ServerT, askModel, catchTCError, findAgdaLib)
3744
import Options (Config)
3845
import qualified Server.Model as Model
3946
import Server.Model.AgdaFile (AgdaFile)
@@ -120,22 +127,6 @@ runWithAgdaLib uri x = do
120127
agdaLib <- Model.getAgdaLib normUri model
121128
runWithAgdaLibT agdaLib x
122129

123-
type NotificationHandlerWithAgdaLib m =
124-
LSP.TNotificationMessage m -> LSP.NormalizedUri -> WithAgdaLibM ()
125-
126-
notificationHandlerWithAgdaLib ::
127-
forall (m :: LSP.Method LSP.ClientToServer LSP.Notification) textdoc.
128-
(LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) =>
129-
LSP.SMethod m ->
130-
NotificationHandlerWithAgdaLib m ->
131-
LSP.Handlers ServerM
132-
notificationHandlerWithAgdaLib m handler = LSP.notificationHandler m $ \notification -> do
133-
let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri
134-
normUri = LSP.toNormalizedUri uri
135-
136-
agdaLib <- findAgdaLib normUri
137-
runWithAgdaLibT agdaLib $ handler notification normUri
138-
139130
instance (MonadIO m) => MonadAgdaLib (WithAgdaLibT m) where
140131
askAgdaLib = WithAgdaLibT ask
141132
localAgdaLib f = WithAgdaLibT . local f . unWithAgdaLibT
@@ -184,31 +175,6 @@ runWithAgdaFileT agdaLib agdaFile =
184175

185176
type WithAgdaFileM = WithAgdaFileT ServerM
186177

187-
type RequestHandlerWithAgdaFile m =
188-
LSP.TRequestMessage m ->
189-
(Either (LSP.TResponseError m) (LSP.MessageResult m) -> WithAgdaFileM ()) ->
190-
WithAgdaFileM ()
191-
192-
requestHandlerWithAgdaFile ::
193-
forall (m :: LSP.Method LSP.ClientToServer LSP.Request).
194-
(LSP.HasTextDocument (LSP.MessageParams m) LSP.TextDocumentIdentifier) =>
195-
LSP.SMethod m ->
196-
RequestHandlerWithAgdaFile m ->
197-
LSP.Handlers ServerM
198-
requestHandlerWithAgdaFile m handler = LSP.requestHandler m $ \req responder -> do
199-
let uri = req ^. LSP.params . LSP.textDocument . LSP.uri
200-
normUri = LSP.toNormalizedUri uri
201-
202-
model <- askModel
203-
case Model.getAgdaFile normUri model of
204-
Nothing -> do
205-
let message = "Request for unknown Agda file at URI: " <> LSP.getUri uri
206-
responder $ Left $ LSP.TResponseError (LSP.InR LSP.ErrorCodes_InvalidParams) message Nothing
207-
Just agdaFile -> do
208-
agdaLib <- Model.getAgdaLib normUri model
209-
let responder' = lift . responder
210-
runWithAgdaFileT agdaLib agdaFile $ handler req responder'
211-
212178
instance (MonadIO m) => MonadAgdaLib (WithAgdaFileT m) where
213179
askAgdaLib = WithAgdaFileT $ view withAgdaFileEnvAgdaLib
214180
localAgdaLib f = WithAgdaFileT . locally withAgdaFileEnvAgdaLib f . unWithAgdaFileT

‎test/Test/ModelMonad.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,8 @@ import Options (Config, defaultOptions, initConfig)
2121
import qualified Server.CommandController as CommandController
2222
import Server.Model (Model)
2323
import Server.Model.AgdaLib (agdaLibIncludes)
24-
import Server.Model.Monad (MonadAgdaLib (askAgdaLib), requestHandlerWithAgdaFile)
24+
import Server.Model.Handler (requestHandlerWithAgdaFile)
25+
import Server.Model.Monad (MonadAgdaLib (askAgdaLib))
2526
import qualified Server.ResponseController as ResponseController
2627
import Test.Tasty (TestTree, testGroup)
2728
import Test.Tasty.HUnit (testCase, (@?), (@?=))

0 commit comments

Comments
 (0)