Skip to content

Commit a2cc346

Browse files
andreasabelandreasabel
committed
WIP: migrate to lsp-2 (does not build yet)
1 parent ccfa2a3 commit a2cc346

File tree

11 files changed

+128
-40
lines changed

11 files changed

+128
-40
lines changed

‎agda-language-server.cabal‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ library
7575
default-extensions:
7676
LambdaCase
7777
OverloadedStrings
78+
PatternSynonyms
7879
TypeOperators
7980
ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans
8081
build-depends:
@@ -83,8 +84,8 @@ library
8384
, base >=4.7 && <5
8485
, bytestring
8586
, containers
86-
, lsp <2
87-
, lsp-types <2
87+
, lsp
88+
, lsp-types
8889
, mtl
8990
, network
9091
, network-simple
@@ -116,6 +117,7 @@ executable als
116117
default-extensions:
117118
LambdaCase
118119
OverloadedStrings
120+
PatternSynonyms
119121
TypeOperators
120122
ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans
121123
build-depends:
@@ -125,8 +127,8 @@ executable als
125127
, base >=4.7 && <5
126128
, bytestring
127129
, containers
128-
, lsp <2
129-
, lsp-types <2
130+
, lsp
131+
, lsp-types
130132
, mtl
131133
, network
132134
, network-simple
@@ -186,6 +188,7 @@ test-suite als-test
186188
default-extensions:
187189
LambdaCase
188190
OverloadedStrings
191+
PatternSynonyms
189192
TypeOperators
190193
ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans
191194
build-depends:
@@ -194,8 +197,8 @@ test-suite als-test
194197
, base >=4.7 && <5
195198
, bytestring
196199
, containers
197-
, lsp <2
198-
, lsp-types <2
200+
, lsp
201+
, lsp-types
199202
, mtl
200203
, network
201204
, network-simple

‎package.yaml‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,8 @@ dependencies:
5555
- aeson
5656
- bytestring
5757
- containers
58-
- lsp-types < 2
59-
- lsp < 2
58+
- lsp-types
59+
- lsp
6060
- mtl
6161
- network
6262
- network-simple
@@ -69,6 +69,7 @@ dependencies:
6969
default-extensions:
7070
- LambdaCase
7171
- OverloadedStrings
72+
- PatternSynonyms
7273
- TypeOperators
7374

7475
library:

‎src/Agda/Parser.hs‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,11 @@ import Data.Maybe (fromMaybe)
1818
import Data.Text (Text, unpack)
1919
import qualified Data.Text as Text
2020
import Language.LSP.Server (LspM)
21-
import qualified Language.LSP.Types as LSP
21+
#if MIN_VERSION_lsp(2,0,0)
22+
import qualified Language.LSP.Protocol.Types as LSP
23+
#else
24+
import qualified Language.LSP.Types as LSP
25+
#endif
2226
import Options (Config)
2327

2428
--------------------------------------------------------------------------------

‎src/Agda/Position.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,11 @@ import qualified Data.Sequence as Seq
2222
import qualified Data.Strict.Maybe as Strict
2323
import Data.Text ( Text )
2424
import qualified Data.Text as Text
25+
#if MIN_VERSION_lsp(2,0,0)
26+
import qualified Language.LSP.Protocol.Types as LSP
27+
#else
2528
import qualified Language.LSP.Types as LSP
29+
#endif
2630

2731
-- Note: LSP srclocs are 0-base
2832
-- Agda srclocs are 1-base

‎src/Monad.hs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1+
{-# LANGUAGE CPP #-}
12
{-# LANGUAGE FlexibleContexts #-}
3+
24
module Monad where
35

46
import Agda.IR
@@ -25,7 +27,11 @@ import Data.Maybe ( isJust )
2527
import Language.LSP.Server ( MonadLsp
2628
, getConfig
2729
)
30+
#if MIN_VERSION_lsp(2,0,0)
31+
import qualified Language.LSP.Protocol.Types as LSP
32+
#else
2833
import qualified Language.LSP.Types as LSP
34+
#endif
2935
import Options
3036

3137
--------------------------------------------------------------------------------

‎src/Server.hs‎

Lines changed: 33 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,29 @@ import qualified Data.Aeson as JSON
1818
import Data.Text ( pack )
1919
import GHC.IO.IOMode ( IOMode(ReadWriteMode) )
2020
import Language.LSP.Server hiding ( Options )
21-
import Language.LSP.Types hiding ( Options(..)
21+
#if MIN_VERSION_lsp(2,0,0)
22+
import Language.LSP.Protocol.Message ( pattern RequestMessage
23+
, SMethod( SMethod_CustomMethod, SMethod_TextDocumentHover)
24+
)
25+
import Language.LSP.Protocol.Types ( TextDocumentSyncOptions(..)
26+
, TextDocumentSyncKind( TextDocumentSyncKind_Incremental )
27+
, ServerCapabilities (_textDocumentSync )
28+
, SaveOptions( SaveOptions )
29+
, pattern TextDocumentIdentifier
30+
, pattern HoverParams
31+
, pattern InR
32+
)
33+
#else
34+
import Language.LSP.Types
35+
hiding ( Options(..)
2236
, TextDocumentSyncClientCapabilities(..)
2337
)
38+
#endif
2439
import Monad
2540
import qualified Network.Simple.TCP as TCP
2641
import Network.Socket ( socketToHandle )
2742
import qualified Switchboard
28-
import Switchboard ( Switchboard )
43+
import Switchboard ( Switchboard, agdaCustomMethod )
2944

3045
import qualified Server.Handler as Handler
3146

@@ -73,7 +88,11 @@ run options = do
7388
}
7489

7590
lspOptions :: LSP.Options
91+
#if MIN_VERSION_lsp_types(2,0,0)
92+
lspOptions = defaultOptions { _textDocumentSync = Just syncOptions }
93+
#else
7694
lspOptions = defaultOptions { textDocumentSync = Just syncOptions }
95+
#endif
7796

7897
-- these `TextDocumentSyncOptions` are essential for receiving notifications from the client
7998
syncOptions :: TextDocumentSyncOptions
@@ -85,7 +104,11 @@ run options = do
85104
}
86105

87106
changeOptions :: TextDocumentSyncKind
107+
#if MIN_VERSION_lsp_types(2,0,0)
108+
changeOptions = TextDocumentSyncKind_Incremental
109+
#else
88110
changeOptions = TdSyncIncremental
111+
#endif
89112

90113
-- includes the document content on save, so that we don't have to read it from the disk
91114
saveOptions :: SaveOptions
@@ -95,13 +118,13 @@ run options = do
95118
handlers :: Handlers (ServerM (LspM Config))
96119
handlers = mconcat
97120
[ -- custom methods, not part of LSP
98-
requestHandler (SCustomMethod "agda") $ \req responder -> do
121+
requestHandler agdaCustomMethod $ \ req responder -> do
99122
let RequestMessage _ _i _ params = req
100123
response <- Agda.sendCommand params
101124
responder $ Right response
102125
,
103126
-- hover provider
104-
requestHandler STextDocumentHover $ \req responder -> do
127+
requestHandler hoverMethod $ \ req responder -> do
105128
let
106129
RequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone)
107130
= req
@@ -112,3 +135,9 @@ handlers = mconcat
112135
-- result <- Handler.onHighlight (req ^. (params . textDocument . uri))
113136
-- responder result
114137
]
138+
where
139+
#if MIN_VERSION_lsp_types(2,0,0)
140+
hoverMethod = SMethod_TextDocumentHover
141+
#else
142+
hoverMethod = STextDocumentHover
143+
#endif

‎src/Server/Handler.hs‎

Lines changed: 20 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,11 @@ import Data.Text ( Text
5555
import qualified Data.Text as Text
5656
import Language.LSP.Server ( LspM )
5757
import qualified Language.LSP.Server as LSP
58+
#if MIN_VERSION_lsp(2,0,0)
59+
import qualified Language.LSP.Protocol.Types as LSP
60+
#else
5861
import qualified Language.LSP.Types as LSP
62+
#endif
5963
import qualified Language.LSP.VFS as VFS
6064
import Monad
6165
import Options ( Config
@@ -124,23 +128,32 @@ onHover uri pos = do
124128
inferResult <- inferTypeOfText filepath text
125129
case inferResult of
126130
Left err -> do
127-
let content = LSP.HoverContents $ LSP.markedUpContent
128-
"agda-language-server"
129-
("Error: " <> pack err)
131+
let content = hoverContent $ "Error: " <> pack err
130132
return $ Just $ LSP.Hover content (Just range)
131133
Right typeString -> do
132-
let content = LSP.HoverContents $ LSP.markedUpContent
133-
"agda-language-server"
134-
(pack typeString)
134+
let content = hoverContent $ pack typeString
135135
return $ Just $ LSP.Hover content (Just range)
136+
where
137+
hoverContent =
138+
#if MIN_VERSION_lsp_types(2,0,0)
139+
LSP.InL . LSP.mkMarkdownCodeBlock "agda-language-server"
140+
#else
141+
LSP.HoverContents . LSP.markedUpContent "agda-language-server"
142+
#endif
136143

137144
--------------------------------------------------------------------------------
138145
-- Helper functions for converting stuff to SemanticTokenAbsolute
139146

140147

141148
fromHighlightingInfo :: IR.HighlightingInfo -> LSP.SemanticTokenAbsolute
142149
fromHighlightingInfo (IR.HighlightingInfo start end aspects isTokenBased note defSrc)
143-
= LSP.SemanticTokenAbsolute 1 1 3 LSP.SttKeyword []
150+
= LSP.SemanticTokenAbsolute 1 1 3 kw []
151+
where
152+
#if MIN_VERSION_lsp_types(2,0,0)
153+
kw = LSP.SemanticTokenTypes_Keyword
154+
#else
155+
kw = LSP.SttKeyword
156+
#endif
144157

145158
-- HighlightingInfo
146159
-- Int -- starting offset

‎src/Switchboard.hs‎

Lines changed: 26 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,12 @@
1-
module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy) where
1+
{-# LANGUAGE CPP #-}
2+
{-# LANGUAGE DataKinds #-}
3+
{-# LANGUAGE PolyKinds #-}
4+
5+
#if MIN_VERSION_lsp_types(2,0,0)
6+
{-# LANGUAGE TypeApplications #-}
7+
#endif
8+
9+
module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy, agdaCustomMethod ) where
210

311
import Monad
412
import Control.Concurrent
@@ -9,7 +17,14 @@ import qualified Agda
917
import qualified Data.Aeson as JSON
1018
import qualified Data.Text.IO as Text
1119
import Language.LSP.Server
12-
import Language.LSP.Types hiding (TextDocumentSyncClientCapabilities (..))
20+
#if MIN_VERSION_lsp(2,0,0)
21+
import Data.Proxy (Proxy(Proxy))
22+
import Language.LSP.Protocol.Message
23+
import Language.LSP.Protocol.Types
24+
#else
25+
import Language.LSP.Types
26+
#endif
27+
hiding (TextDocumentSyncClientCapabilities (..))
1328
import Data.IORef
1429
import Options (Config)
1530

@@ -62,6 +77,14 @@ keepSendindResponse env ctxEnvIORef = forever $ do
6277
callback <- liftIO $ ResponseController.dispatch (envResponseController env)
6378

6479
let value = JSON.toJSON response
65-
sendRequest (SCustomMethod "agda") value $ \_result -> liftIO $ do
80+
sendRequest agdaCustomMethod value $ \_result -> liftIO $ do
6681
-- writeChan (envLogChan env) $ "[Response] >>>> " <> pack (show value)
6782
callback ()
83+
84+
#if MIN_VERSION_lsp_types(2,0,0)
85+
agdaCustomMethod :: SMethod ('Method_CustomMethod "agda")
86+
agdaCustomMethod = SMethod_CustomMethod (Proxy @"agda")
87+
#else
88+
agdaCustomMethod :: SMethod 'CustomMethod
89+
agdaCustomMethod = SCustomMethod "agda"
90+
#endif

‎stack-9.2-Agda-2.6.4.yaml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
resolver: lts-20.26
2+
compiler: ghc-9.2.8
3+
# Allow a newer minor version of GHC than the snapshot specifies
4+
compiler-check: newer-minor
5+
6+
packages:
7+
- .
8+
9+
extra-deps:
10+
- Agda-2.6.4
11+
12+
flags:
13+
Agda:
14+
# optimise-heavily: true
15+
enable-cluster-counting: true

‎stack.yaml‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,11 @@
1-
resolver: lts-20.26
2-
compiler: ghc-9.2.8
1+
resolver: lts-21.22
2+
compiler: ghc-9.4.8
33
# Allow a newer minor version of GHC than the snapshot specifies
44
compiler-check: newer-minor
55

66
packages:
77
- .
88

9-
extra-deps:
10-
- Agda-2.6.4
11-
129
flags:
1310
Agda:
1411
# optimise-heavily: true

0 commit comments

Comments
 (0)