From 7fa662a2ae416898152d7423a92cb1584a476304 Mon Sep 17 00:00:00 2001 From: Ruslan Date: Tue, 29 Aug 2023 22:57:50 +0400 Subject: [PATCH] Split the project into a reusable component library `LSP-lib` and an implementation depending on the library (#202) * Base the code off lib-lsp * Update .gitmodules and README * Update CI * Rename package to `idris2-lsp`; bump package version * Properly (?) add submodule * Update Makefile * Remove a TODO from README --- .github/workflows/ci.yml | 9 +- .gitmodules | 4 + LSP-lib | 1 + Makefile | 6 +- README.md | 8 +- idris2-lsp.ipkg | 13 + lsp.ipkg | 58 -- src/Data/OneOf.idr | 40 -- src/Data/URI.idr | 394 ------------ src/Language/JSON/Interfaces.idr | 213 ------- src/Language/LSP/CodeAction/AddClause.idr | 1 + src/Language/LSP/CodeAction/CaseSplit.idr | 1 + src/Language/LSP/CodeAction/ExprSearch.idr | 1 + src/Language/LSP/CodeAction/GenerateDef.idr | 1 + src/Language/LSP/CodeAction/Intro.idr | 1 + src/Language/LSP/CodeAction/MakeCase.idr | 1 + src/Language/LSP/CodeAction/MakeLemma.idr | 1 + src/Language/LSP/CodeAction/MakeWith.idr | 1 + src/Language/LSP/CodeAction/RefineHole.idr | 5 +- src/Language/LSP/Completion/Handler.idr | 11 +- src/Language/LSP/Definition.idr | 1 + src/Language/LSP/Message.idr | 49 -- src/Language/LSP/Message/CallHierarchy.idr | 93 --- src/Language/LSP/Message/Cancel.idr | 16 - .../LSP/Message/ClientCapabilities.idr | 133 ---- src/Language/LSP/Message/CodeAction.idr | 163 ----- src/Language/LSP/Message/CodeLens.idr | 62 -- src/Language/LSP/Message/Command.idr | 51 -- src/Language/LSP/Message/Completion.idr | 291 --------- src/Language/LSP/Message/Declaration.idr | 46 -- src/Language/LSP/Message/Definition.idr | 79 --- src/Language/LSP/Message/Derive.idr | 211 ------- src/Language/LSP/Message/Diagnostics.idr | 105 ---- src/Language/LSP/Message/DocumentColor.idr | 82 --- .../LSP/Message/DocumentFormatting.idr | 143 ----- .../LSP/Message/DocumentHighlight.idr | 72 --- src/Language/LSP/Message/DocumentLink.idr | 57 -- src/Language/LSP/Message/DocumentSymbols.idr | 219 ------- src/Language/LSP/Message/FoldingRange.idr | 74 --- src/Language/LSP/Message/Hover.idr | 53 -- src/Language/LSP/Message/Implementation.idr | 46 -- src/Language/LSP/Message/Initialize.idr | 60 -- .../LSP/Message/LinkedEditingRange.idr | 52 -- src/Language/LSP/Message/Location.idr | 58 -- src/Language/LSP/Message/Markup.idr | 62 -- src/Language/LSP/Message/Message.idr | 567 ------------------ src/Language/LSP/Message/Method.idr | 337 ----------- src/Language/LSP/Message/Moniker.idr | 94 --- src/Language/LSP/Message/Progress.idr | 61 -- src/Language/LSP/Message/References.idr | 52 -- src/Language/LSP/Message/Registration.idr | 41 -- .../LSP/Message/RegularExpressions.idr | 17 - src/Language/LSP/Message/Rename.idr | 86 --- src/Language/LSP/Message/SelectionRange.idr | 66 -- src/Language/LSP/Message/SemanticTokens.idr | 158 ----- .../LSP/Message/ServerCapabilities.idr | 107 ---- src/Language/LSP/Message/SignatureHelp.idr | 124 ---- src/Language/LSP/Message/TextDocument.idr | 206 ------- src/Language/LSP/Message/Trace.idr | 42 -- src/Language/LSP/Message/URI.idr | 33 - src/Language/LSP/Message/Utils.idr | 85 --- src/Language/LSP/Message/Window.idr | 117 ---- src/Language/LSP/Message/Workspace.idr | 472 --------------- src/Server/Configuration.idr | 2 +- src/Server/Diagnostics.idr | 1 + src/Server/Log.idr | 2 +- src/Server/Main.idr | 3 +- src/Server/ProcessMessage.idr | 5 +- src/Server/Response.idr | 1 + src/Server/Severity.idr | 56 -- src/Server/Utils.idr | 162 ----- src/Server/VirtualDocument.idr | 480 --------------- 72 files changed, 62 insertions(+), 6363 deletions(-) create mode 160000 LSP-lib create mode 100644 idris2-lsp.ipkg delete mode 100644 lsp.ipkg delete mode 100644 src/Data/OneOf.idr delete mode 100644 src/Data/URI.idr delete mode 100644 src/Language/JSON/Interfaces.idr delete mode 100644 src/Language/LSP/Message.idr delete mode 100644 src/Language/LSP/Message/CallHierarchy.idr delete mode 100644 src/Language/LSP/Message/Cancel.idr delete mode 100644 src/Language/LSP/Message/ClientCapabilities.idr delete mode 100644 src/Language/LSP/Message/CodeAction.idr delete mode 100644 src/Language/LSP/Message/CodeLens.idr delete mode 100644 src/Language/LSP/Message/Command.idr delete mode 100644 src/Language/LSP/Message/Completion.idr delete mode 100644 src/Language/LSP/Message/Declaration.idr delete mode 100644 src/Language/LSP/Message/Definition.idr delete mode 100644 src/Language/LSP/Message/Derive.idr delete mode 100644 src/Language/LSP/Message/Diagnostics.idr delete mode 100644 src/Language/LSP/Message/DocumentColor.idr delete mode 100644 src/Language/LSP/Message/DocumentFormatting.idr delete mode 100644 src/Language/LSP/Message/DocumentHighlight.idr delete mode 100644 src/Language/LSP/Message/DocumentLink.idr delete mode 100644 src/Language/LSP/Message/DocumentSymbols.idr delete mode 100644 src/Language/LSP/Message/FoldingRange.idr delete mode 100644 src/Language/LSP/Message/Hover.idr delete mode 100644 src/Language/LSP/Message/Implementation.idr delete mode 100644 src/Language/LSP/Message/Initialize.idr delete mode 100644 src/Language/LSP/Message/LinkedEditingRange.idr delete mode 100644 src/Language/LSP/Message/Location.idr delete mode 100644 src/Language/LSP/Message/Markup.idr delete mode 100644 src/Language/LSP/Message/Message.idr delete mode 100644 src/Language/LSP/Message/Method.idr delete mode 100644 src/Language/LSP/Message/Moniker.idr delete mode 100644 src/Language/LSP/Message/Progress.idr delete mode 100644 src/Language/LSP/Message/References.idr delete mode 100644 src/Language/LSP/Message/Registration.idr delete mode 100644 src/Language/LSP/Message/RegularExpressions.idr delete mode 100644 src/Language/LSP/Message/Rename.idr delete mode 100644 src/Language/LSP/Message/SelectionRange.idr delete mode 100644 src/Language/LSP/Message/SemanticTokens.idr delete mode 100644 src/Language/LSP/Message/ServerCapabilities.idr delete mode 100644 src/Language/LSP/Message/SignatureHelp.idr delete mode 100644 src/Language/LSP/Message/TextDocument.idr delete mode 100644 src/Language/LSP/Message/Trace.idr delete mode 100644 src/Language/LSP/Message/URI.idr delete mode 100644 src/Language/LSP/Message/Utils.idr delete mode 100644 src/Language/LSP/Message/Window.idr delete mode 100644 src/Language/LSP/Message/Workspace.idr delete mode 100644 src/Server/Severity.idr delete mode 100644 src/Server/VirtualDocument.idr diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5e1c915..95c107f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,7 +13,7 @@ env: SCHEME: scheme jobs: - build-idris2-with-api: + build-idris2-with-api: runs-on: ubuntu-latest env: IDRIS2_CG: chez @@ -72,6 +72,13 @@ jobs: sudo apt-get install -y chezscheme echo "$HOME/.idris2/bin" >> $GITHUB_PATH chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/* + - name: Get LSP-lib submodule + run: | + git submodule update --init LSP-lib + - name: Build and install LSP-lib + working-directory: LSP-lib + run: | + idris2 --install-with-src - name: build and test run: | make build && make test INTERACTIVE='' diff --git a/.gitmodules b/.gitmodules index 4992a92..c59e945 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,7 @@ [submodule "Idris2"] path = Idris2 url = https://github.com/idris-lang/Idris2 + +[submodule "LSP-lib"] + path = LSP-lib + url = https://github.com/idris-community/LSP-lib diff --git a/LSP-lib b/LSP-lib new file mode 160000 index 0000000..fa2b656 --- /dev/null +++ b/LSP-lib @@ -0,0 +1 @@ +Subproject commit fa2b6569a0b310aebc91b1e8a32956bcb78629bc diff --git a/Makefile b/Makefile index 20024d4..9e0b1f6 100644 --- a/Makefile +++ b/Makefile @@ -22,14 +22,14 @@ VERSION_TAG ?= $(GIT_SHA1) .PHONY: build FORCE build: src/Server/Generated.idr - $(IDRIS2) --build lsp.ipkg + $(IDRIS2) --build idris2-lsp.ipkg clean: - $(IDRIS2) --clean lsp.ipkg + $(IDRIS2) --clean idris2-lsp.ipkg $(RM) -r build repl: src/Server/Generated.idr - rlwrap $(IDRIS2) --repl lsp.ipkg + rlwrap $(IDRIS2) --repl idris2-lsp.ipkg testbin: @${MAKE} -C tests testbin diff --git a/README.md b/README.md index 8755bf1..d93b35b 100644 --- a/README.md +++ b/README.md @@ -1,11 +1,11 @@ -# [WIP] idris2-lsp +# idris2-lsp Language Server for Idris2. **NOTE: At this stage the LSP server requires an ipkg file to work correctly, for reference material about packages look [here](https://idris2.readthedocs.io/en/latest/tutorial/packages.html) and [here](https://idris2.readthedocs.io/en/latest/reference/packages.html). To start a new project with an ipkg, even for a single file, you can issue the `idris2 --init` command, which provides an interactive interface for package creation.** ## Installation with [Pack](https://github.com/stefan-hoeck/idris2-pack) (Recommended) ```bash -pack install-app lsp +pack install-app idris2-lsp ``` ## Manual Installation @@ -24,6 +24,10 @@ make install # Install Idris make install-with-src-libs # Install sources for libraries make install-with-src-api # Install the API with sources cd .. # Go back to the idris2-lsp directory +git submodule update --init LSP-lib # Get the associated LSP-lib commit +cd LSP-lib +idris2 --install-with-src # Install the LSP library +cd .. # Go back to the idris2-lsp directory make install # Install idris2-lsp ``` diff --git a/idris2-lsp.ipkg b/idris2-lsp.ipkg new file mode 100644 index 0000000..99cc37d --- /dev/null +++ b/idris2-lsp.ipkg @@ -0,0 +1,13 @@ +package idris2-lsp +version = 0.6.0 + +opts = "-Wno-shadowing" + +depends = idris2, contrib, lsp-lib + +sourcedir = "src" + +main = Server.Main +executable = idris2-lsp + +prebuild = "make src/Server/Generated.idr" diff --git a/lsp.ipkg b/lsp.ipkg deleted file mode 100644 index 3caf496..0000000 --- a/lsp.ipkg +++ /dev/null @@ -1,58 +0,0 @@ -package lsp -version = 0.5.0 - -opts = "-Wno-shadowing" - -depends = idris2, contrib - -sourcedir = "src" - -main = Server.Main -executable = idris2-lsp - -modules = Data.URI - , Language.JSON.Interfaces - , Language.LSP.Message - , Language.LSP.Message.CallHierarchy - , Language.LSP.Message.Cancel - , Language.LSP.Message.ClientCapabilities - , Language.LSP.Message.CodeAction - , Language.LSP.Message.CodeLens - , Language.LSP.Message.Command - , Language.LSP.Message.Completion - , Language.LSP.Message.Declaration - , Language.LSP.Message.Definition - , Language.LSP.Message.Derive - , Language.LSP.Message.Diagnostics - , Language.LSP.Message.DocumentColor - , Language.LSP.Message.DocumentFormatting - , Language.LSP.Message.DocumentHighlight - , Language.LSP.Message.DocumentLink - , Language.LSP.Message.DocumentSymbols - , Language.LSP.Message.FoldingRange - , Language.LSP.Message.Hover - , Language.LSP.Message.Implementation - , Language.LSP.Message.Initialize - , Language.LSP.Message.LinkedEditingRange - , Language.LSP.Message.Location - , Language.LSP.Message.Markup - , Language.LSP.Message.Message - , Language.LSP.Message.Method - , Language.LSP.Message.Moniker - , Language.LSP.Message.Progress - , Language.LSP.Message.References - , Language.LSP.Message.Registration - , Language.LSP.Message.RegularExpressions - , Language.LSP.Message.Rename - , Language.LSP.Message.SelectionRange - , Language.LSP.Message.SemanticTokens - , Language.LSP.Message.ServerCapabilities - , Language.LSP.Message.SignatureHelp - , Language.LSP.Message.TextDocument - , Language.LSP.Message.Trace - , Language.LSP.Message.URI - , Language.LSP.Message.Utils - , Language.LSP.Message.Window - , Language.LSP.Message.Workspace - -prebuild = "make src/Server/Generated.idr" diff --git a/src/Data/OneOf.idr b/src/Data/OneOf.idr deleted file mode 100644 index 9ea810e..0000000 --- a/src/Data/OneOf.idr +++ /dev/null @@ -1,40 +0,0 @@ -module Data.OneOf - -import public Data.List.Elem -import public Data.List.Quantifiers - -%default total - -public export -data OneOf : List Type -> Type where - Here : x -> OneOf (x :: xs) - There : OneOf xs -> OneOf (x :: xs) - -public export -make : Elem a as => a -> OneOf as -make x @{Here} = Here x -make x @{There _} = There (make x) - -public export -TypeAt : (as : List Type) -> OneOf as -> Type -TypeAt (x :: _) (Here _) = x -TypeAt (_ :: xs) (There x) = TypeAt xs x - -public export -Eliminators : (as : List Type) -> (r : Type) -> Type -Eliminators xs r = HList (map (\x => x -> r) xs) - -public export -get : (o : OneOf as) -> TypeAt as o -get (Here x) = x -get (There x) = get x - -public export -match : OneOf as -> Eliminators as r -> r -match (Here x) (f :: _) = f x -match (There x) (_ :: fs) = match x fs - -public export -extend : OneOf as -> OneOf (as ++ bs) -extend (Here x) = Here x -extend (There x) = There (extend x) diff --git a/src/Data/URI.idr b/src/Data/URI.idr deleted file mode 100644 index 57bf932..0000000 --- a/src/Data/URI.idr +++ /dev/null @@ -1,394 +0,0 @@ -||| Module for parsing and handling of URIs. -||| -||| References: -||| [1] https://tools.ietf.org/html/rfc3986 -||| [2] https://tools.ietf.org/html/rfc6874 -||| [3] https://tools.ietf.org/html/rfc7320 -||| [4] https://tools.ietf.org/html/rfc8820 -||| -||| (C) The Idris Community, 2021 -module Data.URI - -import Data.Bits -import Data.DPair -import Data.List -import Data.List1 -import Data.Maybe -import Data.String -import Data.String.Extra -import Data.String.Parser -import Data.Vect -import Protocol.Hex - -listElem : Eq a => a -> List a -> Bool -listElem = elem - -foldSeq : (Applicative f, Traversable t, Monoid m) => t (f m) -> f m -foldSeq = map concat . sequence - -||| Type of an authority within URIs. -public export -record URIAuthority where - constructor MkURIAuthority - userInfo : Maybe String - regName : String - port : Maybe Nat - -export -Show URIAuthority where - show authority = - let info = maybe "" (+> '@') authority.userInfo - port = maybe "" ((':' <+) . show) authority.port - in "\{info}\{authority.regName}\{port}" - -export -Eq URIAuthority where - x == y = show x == show y - -export -Ord URIAuthority where - compare x y = compare (show x) (show y) - -||| Type for a general URI. -public export -record URI where - constructor MkURI - scheme : String - authority : Maybe URIAuthority - path : String - query : String - fragment : String - -export -Show URI where - show uri = - let auth = maybe "" ((++ "//") . show) uri.authority - query = if uri.query == "" then "" else '?' <+ uri.query - fragment = if uri.fragment == "" then "" else '#' <+ uri.fragment - in "\{uri.scheme}:\{auth}\{uri.path}\{query}\{fragment}" - -export -Eq URI where - x == y = show x == show y - -export -Ord URI where - compare x y = compare (show x) (show y) - -||| Returns true for characters that are allowed in a URI but do not have a reserved purpose. -||| -||| @see RFC 3986, section 2.3 -isUnreserved : Char -> Bool -isUnreserved c = isAlphaNum c || (c `listElem` ['-', '.', '_', '~']) - -isGenDelim : Char -> Bool -isGenDelim c = c `listElem` [':', '/', '?', '#', '[', ']', '@'] - -||| Returns true for reserved characters that requires to be percent escaped. -||| -||| @see RFC 3986, section 2.2 -isSubDelim : Char -> Bool -isSubDelim c = c `listElem` ['!', '$', '&', '\'', '(', ')', '*', '+', ',', ';', '='] - -isReserved : Char -> Bool -isReserved c = isGenDelim c || isSubDelim c - -||| Parser for percent encoded characters. -||| -||| @see RFC 3986, section 2.1 -pctEncoded : Parser Char -pctEncoded = do - ignore $ char '%' - x <- satisfy isHexDigit - y <- satisfy isHexDigit - let Just d = fromHexChars [y, x] - | Nothing => fail "Cannot convert \{show x}\{show y} to a hex number" - pure $ chr (cast d) - -||| Parser for a URI scheme. -||| -||| @see RFC 3986, section 3.1 -schemeParser : Parser String -schemeParser = pack <$> [| alphaNum :: many (satisfy isValidForScheme) |] - where isValidForScheme : Char -> Bool - isValidForScheme c = isAlphaNum c || (c `listElem` ['+', '-', '.']) - -||| Parser for a URI userinfo subcomponent. -||| -||| @see RFC 3986, section 3.2.1 -userInfoParser : Parser String -userInfoParser = pack <$> many (satisfy isUnreserved <|> char ':' <|> pctEncoded <|> satisfy isSubDelim) - -||| Parser for potentially future version of IPs. -||| -||| @see RFC 3986, section 3.2.2 -ipVFutureParser : Parser String -ipVFutureParser = with Prelude.(::) - foldSeq [ string "v" - , pack <$> some (satisfy isHexDigit) - , string "." - , pack <$> some (satisfy (\c => isUnreserved c || isSubDelim c || c == ':')) - ] - -||| Parser for an IPv4 address. -||| -||| @see RFC 3986, section 3.2.2 -ipV4AddressParser : Parser String -ipV4AddressParser = with Prelude.(::) foldSeq [octet, string ".", octet, string ".", octet, string ".", octet] - where - octet : Parser String - octet = integer >>= (\v => guard (0 <= v && v <= 255) *> pure (show v)) - -||| Parser for an IPv6 address. -||| -||| @see RFC 3986, section 3.2.2 -ipV6AddressParser : Parser String -ipV6AddressParser = with Prelude.(::) - -- This implementation follows closely the definition in the RFC 3986, so is a mess and surely can be improved :( - multipleH16LS32 6 - <|> foldSeq [string "::", multipleH16LS32 5] - <|> foldSeq [optionMap "" id h16, string "::", multipleH16LS32 4] - <|> foldSeq [optionMap "" id (multipleH16 1), string "::", multipleH16LS32 3] - <|> foldSeq [optionMap "" id (multipleH16 2), string "::", multipleH16LS32 2] - <|> foldSeq [optionMap "" id (multipleH16 3), string "::", [| h16 +> char ':' |], ls32] - <|> foldSeq [optionMap "" id (multipleH16 4), string "::", ls32] - <|> foldSeq [optionMap "" id (multipleH16 5), string "::", h16] - <|> foldSeq [optionMap "" id (multipleH16 6), string "::"] - where - h16 : Parser String - h16 = do - c <- satisfy isHexDigit - o1 <- optional (satisfy isHexDigit) - o2 <- optional (satisfy isHexDigit) - o3 <- optional (satisfy isHexDigit) - pure $ pack (c :: fromMaybe [] (sequence [o1, o2, o3])) - - ls32 : Parser String - ls32 = [| [| h16 +> char ':' |] ++ h16 |] <|> ipV4AddressParser - - multipleH16 : Nat -> Parser String - multipleH16 n = [| (concat . toList <$> ntimes n [| h16 +> char ':' |]) ++ h16 |] - - multipleH16LS32 : Nat -> Parser String - multipleH16LS32 n = [| (concat . toList <$> ntimes n [| h16 +> char ':' |]) ++ ls32 |] - -||| Parser for a zone indentifier for a IPv6 Scoped Address. -||| -||| @see RFC 6874, section 2 -zoneIDParser : Parser String -zoneIDParser = pack <$> some (satisfy isUnreserved <|> pctEncoded) - -||| Parser for a IPv6 Scoped Address. -||| -||| @see RFC 6874, section 2 -ipV6AddrzParser : Parser String -ipV6AddrzParser = with Prelude.(::) concat <$> sequence [ipV6AddressParser, string "%25", zoneIDParser] - -||| Parser for a IPv6 Scoped Address. -||| -||| @see RFC 3986, section 3.2.2 -||| @see RFC 6874, section 2 -ipLiteralParser : Parser String -ipLiteralParser = char '[' *> (ipV6AddressParser <|> ipV6AddrzParser <|> ipVFutureParser) <* char ']' - -||| Parser for a registered name. -||| -||| @see RFC 3986, section 3.2.2 -regNameParser : Parser String -regNameParser = pack <$> many (satisfy isUnreserved <|> pctEncoded <|> satisfy isSubDelim) - -||| Parser for a URI authority. -||| -||| @see RFC 3986, section 3.2 -authorityParser : Parser URIAuthority -authorityParser = do - ignore $ string "//" - userInfo <- optional $ userInfoParser <* char '@' - host <- ipLiteralParser <|> ipV4AddressParser <|> regNameParser - port <- optional $ char ':' *> natural - pure $ MkURIAuthority userInfo host port - -||| Parser for a valid character in a path. -||| -||| @see RFC 3986, section 3.3 -pchar : Parser Char -pchar = satisfy (\c => isUnreserved c || isSubDelim c) <|> pctEncoded <|> char ':' <|> char '@' - -||| Parser for a segment in a path. -||| -||| @see RFC 3986, section 3.3 -segment : Parser String -segment = pack <$> many pchar - -||| Parser for a non-empty segment in a path. -||| -||| @see RFC 3986, section 3.3 -segmentNZ : Parser String -segmentNZ = pack <$> some pchar - -||| Parser for a non-empty segment in a path that does not start with a colon. -||| -||| @see RFC 3986, section 3.3 -segmentNZNC : Parser String -segmentNZNC = pack <$> some (satisfy (\c => isUnreserved c || isSubDelim c) <|> pctEncoded <|> char '@') - -||| Parser for an absolute or empty path. -||| -||| @see RFC 3986, section 3.3 -abempty : Parser String -abempty = concat <$> many [| char '/' <+ segment |] - -||| Parser for an absolute path. -||| -||| @see RFC 3986, section 3.3 -absolute : Parser String -absolute = [| char '/' <+ optionMap "" id [| segmentNZ ++ (concat <$> many [| char '/' <+ segment |]) |] |] - -||| Parser for path that starts without a colon. -||| -||| @see RFC 3986, section 3.3 -noscheme : Parser String -noscheme = [| segmentNZNC ++ (concat <$> many [| char '/' <+ segment |]) |] - -||| Parser for path that starts with a segment. -||| -||| @see RFC 3986, section 3.3 -rootless : Parser String -rootless = [| segmentNZ ++ (concat <$> many [| char '/' <+ segment |]) |] - -||| Parser for a, possibly empty, path. -||| -||| @see RFC 3986, section 3.3 -pathParser : Parser String -pathParser = absolute <|> noscheme <|> rootless <|> abempty <|> pure "" - -||| Parser for a query component. -||| -||| @see RFC 3986, section 3.4 -queryParser : Parser String -queryParser = pack <$> many (pchar <|> char '/' <|> char '?') - -||| Parser for a fragment identifier component. -||| -||| @see RFC 3986, section 3.5 -fragmentParser : Parser String -fragmentParser = pack <$> many (pchar <|> char '/' <|> char '?') - -||| Parser for a generic URI. -||| -||| @see RFC 3986, section 3 -export -uriParser : Parser URI -uriParser = do - scheme <- schemeParser - ignore $ char ':' - (authority, path) <- [| MkPair (Just <$> authorityParser) abempty |] <|> ((Nothing,) <$> (absolute <|> rootless <|> empty)) - query <- optionMap "" id (char '?' *> queryParser) - fragment <- optionMap "" id (char '#' *> fragmentParser) - pure $ MkURI scheme authority path query fragment - -||| Parser for a URI relative reference. -||| -||| @see RFC 3986, section 4.2 -relativeReferenceParser : Parser URI -relativeReferenceParser = do - (authority, path) <- [| MkPair (Just <$> authorityParser) abempty |] <|> ((Nothing,) <$> (absolute <|> noscheme <|> empty)) - query <- optionMap "" id (char '?' *> queryParser) - fragment <- optionMap "" id (char '#' *> fragmentParser) - pure $ MkURI "" authority path query fragment - -||| Parser for a URI reference. -||| -||| @see RFC 3986, section 4.1 -export -uriReferenceParser : Parser URI -uriReferenceParser = uriParser <|> relativeReferenceParser - -||| Parser for an absolute URI without a fragment identifier. -||| -||| @see RFC 3986, section 4.3 -export -uriAbsoluteParser : Parser URI -uriAbsoluteParser = do - scheme <- schemeParser - ignore $ char ':' - (authority, path) <- [| MkPair (Just <$> authorityParser) abempty |] <|> ((Nothing,) <$> (absolute <|> rootless <|> empty)) - query <- optionMap "" id (char '?' *> queryParser) - pure $ MkURI scheme authority path query "" - -export -uriIsAbsolute : URI -> Bool -uriIsAbsolute (MkURI {scheme, _}) = scheme /= "" - -export -uriIsRelative : URI -> Bool -uriIsRelative = not . uriIsAbsolute - -export -isUnescapedInURI : Char -> Bool -isUnescapedInURI c = isReserved c || isUnreserved c - -export -isUnescapedInURIComponent : Char -> Bool -isUnescapedInURIComponent c = not (isReserved c || not (isUnescapedInURI c)) - -utf8EncodeChar : Char -> List Int -utf8EncodeChar = go . ord - where - go : Int -> List Int - go x = if x <= 0x7f then [x] - else if x <= 0x7ff then [ 0xc0 + (x `shiftR` 6) - , 0x80 + x .&. 0x3f - ] - else if x <= 0xffff then [ 0xe0 + (x `shiftR` 12) - , 0x80 + ((x `shiftR` 6) .&. 0x3f) - , 0x80 + x .&. 0x3f - ] - else [ 0xf0 + (x `shiftR` 18) - , 0x80 + ((x `shiftR` 12) .&. 0x3f) - , 0x80 + ((x `shiftR` 6) .&. 0x3f) - , 0x80 + x .&. 0x3f - ] - -b16ToHexString : Bits16 -> String -b16ToHexString n = - case n of - 0 => "0" - 1 => "1" - 2 => "2" - 3 => "3" - 4 => "4" - 5 => "5" - 6 => "6" - 7 => "7" - 8 => "8" - 9 => "9" - 10 => "A" - 11 => "B" - 12 => "C" - 13 => "D" - 14 => "E" - 15 => "F" - other => assert_total $ b16ToHexString (n `shiftR` 4) ++ b16ToHexString (n .&. 15) - -pad2 : String -> String -pad2 str = - case length str of - 0 => "00" - 1 => strCons '0' str - _ => str - -export -escapeURIChar : (Char -> Bool) -> Char -> String -escapeURIChar p c = - if p c - then cast c - else concatMap (strCons '%' . pad2 . b16ToHexString . cast) (utf8EncodeChar c) - -export -escapeURIString : (Char -> Bool) -> String -> String -escapeURIString p = foldl (\acc, c => acc ++ escapeURIChar p c) "" . unpack - -export -escapeAndParseURI : String -> Either String URI -escapeAndParseURI = mapSnd fst . parse (uriReferenceParser <* eos) . escapeURIString isUnescapedInURI diff --git a/src/Language/JSON/Interfaces.idr b/src/Language/JSON/Interfaces.idr deleted file mode 100644 index 4fc0e4b..0000000 --- a/src/Language/JSON/Interfaces.idr +++ /dev/null @@ -1,213 +0,0 @@ -||| Interfaces for converting values from/to JSON. -||| -||| (C) The Idris Community, 2021 -module Language.JSON.Interfaces - -import Data.SortedMap -import Data.String -import Language.JSON.Lexer -import Language.JSON.Parser - -import Language.JSON - -%default total - --- TODO: Maybe we should be using a more expressive type than Maybe. -||| A type that can be converted to JSON. -||| An example type and implementation is: -||| ```idris example -||| record Position where -||| constructor MkPosition -||| x : Integer -||| y : Integer -||| -||| ToJSON Position where -||| toJSON pos = JObject [("x", toJSON pos.x), ("y", toJSON pos.y)] -||| ``` -public export -interface ToJSON a where - toJSON : a -> JSON - -||| A type that can be possibly converted from JSON. -||| An example type and implementation is: -||| ```idris example -||| record Position where -||| constructor MkPosition -||| x : Integer -||| y : Integer -||| -||| FromJSON Position where -||| fromJSON (JObject arg) = do -||| x <- lookup "x" arg >>= fromJSON -||| y <- lookup "y" arg >>= fromJSON -||| pure $ MkPosition x y -||| fromJSON _ = neutral -||| ``` -public export -interface FromJSON a where - fromJSON : JSON -> Maybe a - -export -ToJSON JSON where - toJSON = id - -export -FromJSON JSON where - fromJSON = pure - -export -ToJSON Integer where - toJSON = JNumber . cast - --- NOTE: In JSON all numbers are `Double`, for integers we should cast or fail --- for invalid values? -export -FromJSON Integer where - fromJSON (JNumber x) = pure (cast x) - fromJSON _ = neutral - -export -ToJSON Int where - toJSON = JNumber . cast - -export -FromJSON Int where - fromJSON (JNumber x) = pure (cast x) - fromJSON _ = neutral - -export -ToJSON Bits8 where - toJSON = JNumber . cast . cast {to = Int} - -export -FromJSON Bits8 where - fromJSON (JNumber x) = pure (fromInteger $ cast x) - fromJSON _ = neutral - -export -ToJSON Bits16 where - toJSON = JNumber . cast . cast {to = Int} - -export -FromJSON Bits16 where - fromJSON (JNumber x) = pure (fromInteger $ cast x) - fromJSON _ = neutral - -export -ToJSON Bits32 where - toJSON = JNumber . cast . cast {to = Int} - -export -FromJSON Bits32 where - fromJSON (JNumber x) = pure (fromInteger $ cast x) - fromJSON _ = neutral - -export -ToJSON Bits64 where - toJSON = JNumber . cast . cast {to = Int} - -export -FromJSON Bits64 where - fromJSON (JNumber x) = pure (fromInteger $ cast x) - fromJSON _ = neutral - -export -ToJSON Double where - toJSON = JNumber - -export -FromJSON Double where - fromJSON (JNumber x) = pure x - fromJSON _ = neutral - -export -ToJSON Nat where - toJSON = JNumber . cast - -export -FromJSON Nat where - fromJSON (JNumber x) = pure (fromInteger $ cast x) - fromJSON _ = neutral - -export -ToJSON String where - toJSON = JString - -export -FromJSON String where - fromJSON (JString s) = pure s - fromJSON _ = neutral - -export -ToJSON Char where - toJSON = toJSON . String.singleton - -export -FromJSON Char where - fromJSON (JString s) = case strM s of - StrCons c "" => pure c - _ => neutral - fromJSON _ = neutral - -export -ToJSON Bool where - toJSON = JBoolean - -export -FromJSON Bool where - fromJSON (JBoolean b) = pure b - fromJSON _ = neutral - -export -ToJSON a => ToJSON (Maybe a) where - toJSON Nothing = JNull - toJSON (Just x) = toJSON x - -export -FromJSON a => FromJSON (Maybe a) where - fromJSON JNull = pure Nothing - fromJSON json @{impl} = pure <$> fromJSON @{impl} json - -export -ToJSON a => ToJSON (List a) where - toJSON = JArray . map toJSON - -export -FromJSON a => FromJSON (List a) where - fromJSON (JArray xs) = traverse fromJSON xs - fromJSON _ = neutral - -export -ToJSON () where - toJSON () = JObject empty - -export -FromJSON () where - fromJSON (JObject xs) = guard $ null xs - fromJSON _ = neutral - -export -(ToJSON a, ToJSON b) => ToJSON (a, b) where - toJSON (x, y) = JArray [toJSON x, toJSON y] - -export -(FromJSON a, FromJSON b) => FromJSON (a, b) where - fromJSON (JArray [x, y]) = (,) <$> fromJSON x <*> fromJSON y - fromJSON _ = neutral - -export -ToJSON v => ToJSON (SortedMap String v) where - toJSON m = JObject (toList $ toJSON <$> m) - -export -FromJSON v => FromJSON (SortedMap String v) where - fromJSON (JObject xs) = fromList <$> traverse (\(k, v) => (k,) <$> fromJSON v) xs - fromJSON _ = neutral - -export -ToJSON a => ToJSON (Inf a) where - toJSON x = toJSON x - -export -FromJSON a => FromJSON (Inf a) where - fromJSON @{impl} x = map (\x => Delay x) (fromJSON @{impl} x) diff --git a/src/Language/LSP/CodeAction/AddClause.idr b/src/Language/LSP/CodeAction/AddClause.idr index ca5ac27..44d4f88 100644 --- a/src/Language/LSP/CodeAction/AddClause.idr +++ b/src/Language/LSP/CodeAction/AddClause.idr @@ -11,6 +11,7 @@ import Idris.Syntax import Language.JSON import Language.LSP.CodeAction.Utils import Language.LSP.Message +import Language.LSP.Utils import Server.Configuration import Server.Log import Server.Utils diff --git a/src/Language/LSP/CodeAction/CaseSplit.idr b/src/Language/LSP/CodeAction/CaseSplit.idr index e07a263..29b15ba 100644 --- a/src/Language/LSP/CodeAction/CaseSplit.idr +++ b/src/Language/LSP/CodeAction/CaseSplit.idr @@ -12,6 +12,7 @@ import Language.JSON import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message +import Language.LSP.Utils import Server.Configuration import Server.Log import Server.Utils diff --git a/src/Language/LSP/CodeAction/ExprSearch.idr b/src/Language/LSP/CodeAction/ExprSearch.idr index 87976b0..dc620ed 100644 --- a/src/Language/LSP/CodeAction/ExprSearch.idr +++ b/src/Language/LSP/CodeAction/ExprSearch.idr @@ -15,6 +15,7 @@ import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message import Language.LSP.Message.Derive +import Language.LSP.Utils import Language.Reflection import Parser.Rule.Source import Parser.Source diff --git a/src/Language/LSP/CodeAction/GenerateDef.idr b/src/Language/LSP/CodeAction/GenerateDef.idr index 61958b9..74d3e63 100644 --- a/src/Language/LSP/CodeAction/GenerateDef.idr +++ b/src/Language/LSP/CodeAction/GenerateDef.idr @@ -13,6 +13,7 @@ import Language.JSON import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message +import Language.LSP.Utils import Parser.Unlit import Server.Configuration import Server.Log diff --git a/src/Language/LSP/CodeAction/Intro.idr b/src/Language/LSP/CodeAction/Intro.idr index 03bcbb8..d543aed 100644 --- a/src/Language/LSP/CodeAction/Intro.idr +++ b/src/Language/LSP/CodeAction/Intro.idr @@ -14,6 +14,7 @@ import Language.JSON import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message +import Language.LSP.Utils import Server.Configuration import Server.Log import Server.Utils diff --git a/src/Language/LSP/CodeAction/MakeCase.idr b/src/Language/LSP/CodeAction/MakeCase.idr index 87375ac..21d5f2e 100644 --- a/src/Language/LSP/CodeAction/MakeCase.idr +++ b/src/Language/LSP/CodeAction/MakeCase.idr @@ -14,6 +14,7 @@ import Language.JSON import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message +import Language.LSP.Utils import Libraries.Data.PosMap import Parser.Unlit import Server.Configuration diff --git a/src/Language/LSP/CodeAction/MakeLemma.idr b/src/Language/LSP/CodeAction/MakeLemma.idr index b343809..036c097 100644 --- a/src/Language/LSP/CodeAction/MakeLemma.idr +++ b/src/Language/LSP/CodeAction/MakeLemma.idr @@ -13,6 +13,7 @@ import Language.JSON import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message +import Language.LSP.Utils import Libraries.Data.List.Extra import Libraries.Data.PosMap import Parser.Unlit diff --git a/src/Language/LSP/CodeAction/MakeWith.idr b/src/Language/LSP/CodeAction/MakeWith.idr index 03f121f..b6dd166 100644 --- a/src/Language/LSP/CodeAction/MakeWith.idr +++ b/src/Language/LSP/CodeAction/MakeWith.idr @@ -13,6 +13,7 @@ import Language.JSON import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message +import Language.LSP.Utils import Libraries.Data.PosMap import Parser.Unlit import Server.Configuration diff --git a/src/Language/LSP/CodeAction/RefineHole.idr b/src/Language/LSP/CodeAction/RefineHole.idr index a28f092..86216e2 100644 --- a/src/Language/LSP/CodeAction/RefineHole.idr +++ b/src/Language/LSP/CodeAction/RefineHole.idr @@ -18,6 +18,7 @@ import Language.LSP.CodeAction import Language.LSP.CodeAction.Utils import Language.LSP.Message import Language.LSP.Message.Derive +import Language.LSP.Utils import Language.Reflection import Libraries.Data.NameMap import Parser.Source @@ -77,9 +78,9 @@ refineHole : Ref LSPConf LSPConfiguration refineHole params = do let True = isAllowed params.codeAction | False => logI RefineHole "Skipped" >> pure [] - logI RefineHole "Checking for \{show params.codeAction.textDocument.uri} at \{show params.codeAction.range}" + logI RefineHole "Checking for \{show params.codeAction.textDocument.uri} at \{show params.codeAction.range}" withSingleLine RefineHole params.codeAction (pure []) $ \line => do - nameLocs <- gets MD nameLocMap + nameLocs <- gets MD nameLocMap let col = params.codeAction.range.start.character let Just (loc@(_, nstart, nend), holename) = findPointInTreeLoc (line, col) nameLocs | Nothing => logD RefineHole "No name found at \{show line}:\{show col}}" >> pure [] diff --git a/src/Language/LSP/Completion/Handler.idr b/src/Language/LSP/Completion/Handler.idr index e1394e2..6e4227e 100644 --- a/src/Language/LSP/Completion/Handler.idr +++ b/src/Language/LSP/Completion/Handler.idr @@ -16,17 +16,18 @@ import Idris.Syntax import Language.JSON.Data import Language.LSP.Completion.Info import Language.LSP.Message +import Language.LSP.Utils +import Language.LSP.VirtualDocument import Libraries.Data.NameMap import Libraries.Data.UserNameMap import Server.Configuration import Server.Log import Server.Utils -import Server.VirtualDocument %default total -- When a file is opened the context is filled with definitions. --- +-- -- Cache names from opened files. -- Update cache on saving a file. -- Remove cache on closing a file. @@ -108,7 +109,7 @@ completionNames = do mdef <- lookupCtxtExact n ctxt case mdef of Nothing => pure Nothing - Just def => + Just def => let visible = (ns == currentNS defs) || (visibility def /= Private) in if visible then do @@ -123,9 +124,9 @@ completionNames = do , documentation = show doc } else pure Nothing) - inImportedNamespaces + inImportedNamespaces let completionEntries = catMaybes visibleExportedNames - logD Completion "Found \{show (length completionEntries)} completion entries." + logD Completion "Found \{show (length completionEntries)} completion entries." pure $ foldl (\m , c => mergeWith (++) m (singleton c.category [c])) empty completionEntries where accessibleName : List Namespace -> Name -> Maybe (Namespace, UserName, Name) diff --git a/src/Language/LSP/Definition.idr b/src/Language/LSP/Definition.idr index 96d1224..cf5a79c 100644 --- a/src/Language/LSP/Definition.idr +++ b/src/Language/LSP/Definition.idr @@ -11,6 +11,7 @@ import Data.String import Data.String.Parser import Data.URI import Language.LSP.Message +import Language.LSP.Utils import Libraries.Data.PosMap import Server.Configuration import Server.Log diff --git a/src/Language/LSP/Message.idr b/src/Language/LSP/Message.idr deleted file mode 100644 index 6faa78a..0000000 --- a/src/Language/LSP/Message.idr +++ /dev/null @@ -1,49 +0,0 @@ -||| Module for the parsing and encoding LSP messages, updated to version 3.16. -||| -||| References: -||| [1] https://microsoft.github.io/language-server-protocol/specifications/specification-3-16/ -||| -||| (C) The Idris Community, 2021 -module Language.LSP.Message - -import public Language.LSP.Message.CallHierarchy -import public Language.LSP.Message.Cancel -import public Language.LSP.Message.ClientCapabilities -import public Language.LSP.Message.CodeAction -import public Language.LSP.Message.CodeLens -import public Language.LSP.Message.Command -import public Language.LSP.Message.Completion -import public Language.LSP.Message.Declaration -import public Language.LSP.Message.Definition -import public Language.LSP.Message.Derive -import public Language.LSP.Message.Diagnostics -import public Language.LSP.Message.DocumentColor -import public Language.LSP.Message.DocumentFormatting -import public Language.LSP.Message.DocumentHighlight -import public Language.LSP.Message.DocumentLink -import public Language.LSP.Message.DocumentSymbols -import public Language.LSP.Message.FoldingRange -import public Language.LSP.Message.Hover -import public Language.LSP.Message.Implementation -import public Language.LSP.Message.Initialize -import public Language.LSP.Message.LinkedEditingRange -import public Language.LSP.Message.Location -import public Language.LSP.Message.Markup -import public Language.LSP.Message.Message -import public Language.LSP.Message.Method -import public Language.LSP.Message.Moniker -import public Language.LSP.Message.Progress -import public Language.LSP.Message.References -import public Language.LSP.Message.Registration -import public Language.LSP.Message.RegularExpressions -import public Language.LSP.Message.Rename -import public Language.LSP.Message.SelectionRange -import public Language.LSP.Message.SemanticTokens -import public Language.LSP.Message.ServerCapabilities -import public Language.LSP.Message.SignatureHelp -import public Language.LSP.Message.TextDocument -import public Language.LSP.Message.Trace -import public Language.LSP.Message.URI -import public Language.LSP.Message.Utils -import public Language.LSP.Message.Window -import public Language.LSP.Message.Workspace diff --git a/src/Language/LSP/Message/CallHierarchy.idr b/src/Language/LSP/Message/CallHierarchy.idr deleted file mode 100644 index 294ab8b..0000000 --- a/src/Language/LSP/Message/CallHierarchy.idr +++ /dev/null @@ -1,93 +0,0 @@ -module Language.LSP.Message.CallHierarchy - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.DocumentSymbols -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy -public export -record CallHierarchyClientCapabilities where - constructor MkCallHierarchyClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{CallHierarchyClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy -public export -record CallHierarchyOptions where - constructor MkCallHierarchyOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{CallHierarchyOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy -public export -record CallHierarchyRegistrationOptions where - constructor MkCallHierarchyRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe String -%runElab deriveJSON defaultOpts `{CallHierarchyRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy -public export -record CallHierarchyParams where - constructor MkCallHierarchyParams - workDoneToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{CallHierarchyParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareCallHierarchy -public export -record CallHierarchyItem where - constructor MkCallHierarchyItem - name : String - kind : SymbolKind - tags : Maybe (List SymbolTag) - detail : Maybe String - uri : DocumentURI - range : Range - selectionRange : Range - data_ : Maybe JSON -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CallHierarchyItem} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_incomingCalls -public export -record CallHierarchyIncomingCallsParams where - constructor MkCallHierarchyIncomingCallsParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - item : CallHierarchyItem -%runElab deriveJSON defaultOpts `{CallHierarchyIncomingCallsParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_incomingCalls -public export -record CallHierarchyIncomingCall where - constructor MkCallHierarchyIncomingCall - from : CallHierarchyItem - fromRanges : List Range -%runElab deriveJSON defaultOpts `{CallHierarchyIncomingCall} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_outgoingCalls -public export -record CallHierarchyOutgoingCallsParams where - constructor MkCallHierarchyOutgoingCallsParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - item : CallHierarchyItem -%runElab deriveJSON defaultOpts `{CallHierarchyOutgoingCallsParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#callHierarchy_outgoingCalls -public export -record CallHierarchyOutgoingCall where - constructor MkCallHierarchyOutgoingCall - to : CallHierarchyItem - fromRanges : List Range -%runElab deriveJSON defaultOpts `{CallHierarchyOutgoingCall} diff --git a/src/Language/LSP/Message/Cancel.idr b/src/Language/LSP/Message/Cancel.idr deleted file mode 100644 index f00c48d..0000000 --- a/src/Language/LSP/Message/Cancel.idr +++ /dev/null @@ -1,16 +0,0 @@ -module Language.LSP.Message.Cancel - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#cancelRequest -public export -record CancelParams where - constructor MkCancelParams - id : OneOf [Int, String] -%runElab deriveJSON defaultOpts `{CancelParams} diff --git a/src/Language/LSP/Message/ClientCapabilities.idr b/src/Language/LSP/Message/ClientCapabilities.idr deleted file mode 100644 index c8b8645..0000000 --- a/src/Language/LSP/Message/ClientCapabilities.idr +++ /dev/null @@ -1,133 +0,0 @@ -module Language.LSP.Message.ClientCapabilities - -import Language.JSON -import Language.LSP.Message.CallHierarchy -import Language.LSP.Message.Cancel -import Language.LSP.Message.CodeAction -import Language.LSP.Message.CodeLens -import Language.LSP.Message.Command -import Language.LSP.Message.Completion -import Language.LSP.Message.Declaration -import Language.LSP.Message.Definition -import Language.LSP.Message.Derive -import Language.LSP.Message.Diagnostics -import Language.LSP.Message.DocumentColor -import Language.LSP.Message.DocumentFormatting -import Language.LSP.Message.DocumentHighlight -import Language.LSP.Message.DocumentLink -import Language.LSP.Message.DocumentSymbols -import Language.LSP.Message.FoldingRange -import Language.LSP.Message.Hover -import Language.LSP.Message.Implementation -import Language.LSP.Message.LinkedEditingRange -import Language.LSP.Message.Location -import Language.LSP.Message.Markup -import Language.LSP.Message.Method -import Language.LSP.Message.Moniker -import Language.LSP.Message.Progress -import Language.LSP.Message.References -import Language.LSP.Message.Registration -import Language.LSP.Message.RegularExpressions -import Language.LSP.Message.Rename -import Language.LSP.Message.SelectionRange -import Language.LSP.Message.SemanticTokens -import Language.LSP.Message.SignatureHelp -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Trace -import Language.LSP.Message.Utils -import Language.LSP.Message.Window -import Language.LSP.Message.Workspace -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record TextDocumentClientCapabilities where - constructor MkTextDocumentClientCapabilities - synchronization : Maybe TextDocumentSyncClientCapabilities - completion : Maybe CompletionClientCapabilities - hover : Maybe HoverClientCapabilities - signatureHelp : Maybe SignatureHelpClientCapabilities - declaration : Maybe DeclarationClientCapabilities - definition : Maybe DefinitionClientCapabilities - typeDefinition : Maybe TypeDefinitionClientCapabilities - implementation_ : Maybe ImplementationClientCapabilities - references : Maybe ReferenceClientCapabilities - documentHighlight : Maybe DocumentHighlightClientCapabilities - documentSymbol : Maybe DocumentSymbolClientCapabilities - codeAction : Maybe CodeActionClientCapabilities - codeLens : Maybe CodeLensClientCapabilities - documentLink : Maybe DocumentLinkClientCapabilities - colorProvider : Maybe DocumentColorClientCapabilities - formatting : Maybe DocumentFormattingClientCapabilities - rangeFormatting : Maybe DocumentRangeFormattingClientCapabilities - onTypeFormatting : Maybe DocumentOnTypeFormattingClientCapabilities - rename : Maybe RenameClientCapabilities - publishDiagnostics : Maybe PublishDiagnosticsClientCapabilities - foldingRange : Maybe FoldingRangeClientCapabilities - selectionRange : Maybe SelectionRangeClientCapabilities - linkedEditingRange : Maybe LinkedEditingRangeClientCapabilities - callHierarchy : Maybe CallHierarchyClientCapabilities - semanticTokens : Maybe SemanticTokensClientCapabilities - moniker : Maybe MonikerClientCapabilities -%runElab deriveJSON ({renames := [("implementation_", "implementation")]} defaultOpts) `{TextDocumentClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record FileOperationsWorkspaceClientCapabilities where - constructor MkFileOperationsWorkspaceClientCapabilities - dynamicRegistration : Maybe Bool - didCreate : Maybe Bool - willCreate : Maybe Bool - didRename : Maybe Bool - willRename : Maybe Bool - didDelete : Maybe Bool - willDelete : Maybe Bool -%runElab deriveJSON defaultOpts `{FileOperationsWorkspaceClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record WorkspaceClientCapabilities where - constructor MkWorkspaceClientCapabilities - applyEdit : Maybe Bool - workspaceEdit : Maybe WorkspaceEditClientCapabilities - didChangeConfiguration : Maybe DidChangeConfigurationClientCapabilities - didChangeWatchedFiles : Maybe DidChangeWatchedFilesClientCapabilities - symbol : Maybe WorkspaceSymbolClientCapabilities - executeCommand : Maybe ExecuteCommandClientCapabilities - workspaceFolders : Maybe Bool - configuration : Maybe Bool - semanticTokens : Maybe SemanticTokensWorkspaceClientCapabilities - codeLens : Maybe CodeLensWorkspaceClientCapabilities - fileOperations : Maybe FileOperationsWorkspaceClientCapabilities -%runElab deriveJSON defaultOpts `{WorkspaceClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record WindowClientCapabilities where - constructor MkWindowClientCapabilities - workDoneProgress : Maybe Bool - showMessage : Maybe ShowMessageRequestClientCapabilities - showDocument : Maybe ShowDocumentClientCapabilities -%runElab deriveJSON defaultOpts `{WindowClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record GeneralClientCapabilities where - constructor MkGeneralClientCapabilities - regularExpressions : Maybe RegularExpressionsClientCapabilities - markdown : Maybe MarkdownClientCapabilities -%runElab deriveJSON defaultOpts `{GeneralClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record ClientCapabilities where - constructor MkClientCapabilities - workspace : Maybe WorkspaceClientCapabilities - textDocument : Maybe TextDocumentClientCapabilities - window : Maybe WindowClientCapabilities - general : Maybe GeneralClientCapabilities - experimental : Maybe JSON -%runElab deriveJSON defaultOpts `{ClientCapabilities} diff --git a/src/Language/LSP/Message/CodeAction.idr b/src/Language/LSP/Message/CodeAction.idr deleted file mode 100644 index 5a9e545..0000000 --- a/src/Language/LSP/Message/CodeAction.idr +++ /dev/null @@ -1,163 +0,0 @@ -module Language.LSP.Message.CodeAction - -import Language.JSON -import Language.LSP.Message.Command -import Language.LSP.Message.Derive -import Language.LSP.Message.Diagnostics -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.LSP.Message.Workspace -import Language.Reflection - -%language ElabReflection -%default total - -namespace CodeActionKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction - public export - data CodeActionKind - = Empty - | QuickFix - | Refactor - | RefactorExtract - | RefactorInline - | RefactorRewrite - | Source - | SourceOrganizeImport - | Other String - -export -Eq CodeActionKind where - Empty == Empty = True - QuickFix == QuickFix = True - Refactor == Refactor = True - RefactorExtract == RefactorExtract = True - RefactorInline == RefactorInline = True - RefactorRewrite == RefactorRewrite = True - Source == Source = True - SourceOrganizeImport == SourceOrganizeImport = True - (Other str) == (Other str') = str == str' - _ == _ = False - -export -ToJSON CodeActionKind where - toJSON Empty = JString "" - toJSON QuickFix = JString "quickfix" - toJSON Refactor = JString "refactor" - toJSON RefactorExtract = JString "refactor.extract" - toJSON RefactorInline = JString "refactor.inline" - toJSON RefactorRewrite = JString "refactor.rewrite" - toJSON Source = JString "source" - toJSON SourceOrganizeImport = JString "source.organizeImports" - toJSON (Other act) = JString act - -export -FromJSON CodeActionKind where - fromJSON (JString "") = pure Empty - fromJSON (JString "quickfix") = pure QuickFix - fromJSON (JString "refactor") = pure Refactor - fromJSON (JString "refactor.extract") = pure RefactorExtract - fromJSON (JString "refactor.inline") = pure RefactorInline - fromJSON (JString "refactor.rewrite") = pure RefactorRewrite - fromJSON (JString "source") = pure Source - fromJSON (JString "source.organizeImports") = pure SourceOrganizeImport - fromJSON (JString act) = pure (Other act) - fromJSON _ = neutral - -namespace CodeActionClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction - public export - record CodeActionKindValueSet where - constructor MkCodeActionKindValueSet - valueSet : List CodeActionKind - %runElab deriveJSON defaultOpts `{CodeActionKindValueSet} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction - public export - record CodeActionLiteralSupport where - constructor MkCodeActionLiteralSupport - codeActionKind : CodeActionKindValueSet - %runElab deriveJSON defaultOpts `{CodeActionLiteralSupport} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction - public export - record ResolveSupport where - constructor MkResolveSupport - properties : List String - %runElab deriveJSON defaultOpts `{ResolveSupport} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction -public export -record CodeActionClientCapabilities where - constructor MkCodeActionClientCapabilities - dynamicRegistration : Maybe Bool - codeActionLiteralSupport : Maybe CodeActionLiteralSupport - isPreferredSupport : Maybe Bool - disabledSupport : Maybe Bool - dataSupport : Maybe Bool - resolveSupport : Maybe ResolveSupport - honorsChangeAnnotations : Maybe Bool -%runElab deriveJSON defaultOpts `{CodeActionClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction -public export -record CodeActionOptions where - constructor MkCodeActionOptions - workDoneProgress : Maybe Bool - codeActionKinds : Maybe (List CodeActionKind) - resolveProvider : Maybe Bool -%runElab deriveJSON defaultOpts `{CodeActionOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction -public export -record CodeActionRegistrationOptions where - constructor MkCodeActionRegistrationOptions - workDoneProgress : Maybe Bool - codeActionKinds : Maybe (List CodeActionKind) - resolveProvider : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{CodeActionRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction -public export -record CodeActionContext where - constructor MkCodeActionContext - diagnostics : List Diagnostic - only : Maybe (List CodeActionKind) -%runElab deriveJSON defaultOpts `{CodeActionContext} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction -public export -record CodeActionParams where - constructor MkCodeActionParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - range : Range - context : CodeActionContext -%runElab deriveJSON defaultOpts `{CodeActionParams} - -namespace CodeAction - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction - public export - record Disabled where - constructor MkDisabled - reason : String - %runElab deriveJSON defaultOpts `{Disabled} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction -public export -record CodeAction where - constructor MkCodeAction - title : String - kind : Maybe CodeActionKind - diagnostics : Maybe (List Diagnostic) - isPreferred : Maybe Bool - disabled : Maybe Disabled - edit : Maybe WorkspaceEdit - command : Maybe Command - data_ : Maybe JSON -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CodeAction} diff --git a/src/Language/LSP/Message/CodeLens.idr b/src/Language/LSP/Message/CodeLens.idr deleted file mode 100644 index 6df175e..0000000 --- a/src/Language/LSP/Message/CodeLens.idr +++ /dev/null @@ -1,62 +0,0 @@ -module Language.LSP.Message.CodeLens - -import Language.JSON -import Language.LSP.Message.Command -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens -public export -record CodeLensClientCapabilities where - constructor MkCodeLensClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{CodeLensClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens -public export -record CodeLensOptions where - constructor MkCodeLensOptions - workDoneProgress : Maybe Bool - resolveProvider : Maybe Bool -%runElab deriveJSON defaultOpts `{CodeLensOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens -public export -record CodeLensRegistrationOptions where - constructor MkCodeLensRegistrationOptions - workDoneProgress : Maybe Bool - resolveProvider : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{CodeLensRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens -public export -record CodeLensParams where - constructor MkCodeLensParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{CodeLensParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens -public export -record CodeLens where - constructor MkCodeLens - range : Range - command : Maybe Command - data_ : Maybe JSON -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CodeLens} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#codeLens_refresh -public export -record CodeLensWorkspaceClientCapabilities where - constructor MkCodeLensWorkspaceClientCapabilities - refreshSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{CodeLensWorkspaceClientCapabilities} diff --git a/src/Language/LSP/Message/Command.idr b/src/Language/LSP/Message/Command.idr deleted file mode 100644 index 5728db9..0000000 --- a/src/Language/LSP/Message/Command.idr +++ /dev/null @@ -1,51 +0,0 @@ -module Language.LSP.Message.Command - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Progress -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#command -public export -record Command where - constructor MkCommand - title : String - command : String - arguments : Maybe (List JSON) -%runElab deriveJSON defaultOpts `{Command} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand -public export -record ExecuteCommandClientCapabilities where - constructor MkExecuteCommandClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{ExecuteCommandClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand -public export -record ExecuteCommandOptions where - constructor MkExecuteCommandOptions - workDoneProgress : Maybe Bool - commands : List String -%runElab deriveJSON defaultOpts `{ExecuteCommandOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand -public export -record ExecuteCommandRegistrationOptions where - constructor MkExecuteCommandRegistrationOptions - workDoneProgress : Maybe Bool - commands : List String -%runElab deriveJSON defaultOpts `{ExecuteCommandRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand -public export -record ExecuteCommandParams where - constructor MkExecuteCommandParams - partialResultToken : Maybe ProgressToken - command : String - arguments : Maybe (List JSON) -%runElab deriveJSON defaultOpts `{ExecuteCommandParams} diff --git a/src/Language/LSP/Message/Completion.idr b/src/Language/LSP/Message/Completion.idr deleted file mode 100644 index 9a13dd5..0000000 --- a/src/Language/LSP/Message/Completion.idr +++ /dev/null @@ -1,291 +0,0 @@ -module Language.LSP.Message.Completion - -import Language.JSON -import Language.LSP.Message.Command -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Markup -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.LSP.Message.Workspace -import Language.Reflection - -%language ElabReflection -%default total - -namespace CompletionItemKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - data CompletionItemKind - = Text - | Method - | Function - | Constructor - | Field - | Variable - | Class - | Interface - | Module - | Property - | Unit_ - | Value - | Enum - | Keyword - | Snippet - | Color - | File - | Reference - | Folder - | EnumMember - | Constant - | Struct - | Event - | Operator - | TypeParameter - -export -ToJSON CompletionItemKind where - toJSON Text = JNumber 1 - toJSON Method = JNumber 2 - toJSON Function = JNumber 3 - toJSON Constructor = JNumber 4 - toJSON Field = JNumber 5 - toJSON Variable = JNumber 6 - toJSON Class = JNumber 7 - toJSON Interface = JNumber 8 - toJSON Module = JNumber 9 - toJSON Property = JNumber 10 - toJSON Unit_ = JNumber 11 - toJSON Value = JNumber 12 - toJSON Enum = JNumber 13 - toJSON Keyword = JNumber 14 - toJSON Snippet = JNumber 15 - toJSON Color = JNumber 16 - toJSON File = JNumber 17 - toJSON Reference = JNumber 18 - toJSON Folder = JNumber 19 - toJSON EnumMember = JNumber 20 - toJSON Constant = JNumber 21 - toJSON Struct = JNumber 22 - toJSON Event = JNumber 23 - toJSON Operator = JNumber 24 - toJSON TypeParameter = JNumber 25 - -export -FromJSON CompletionItemKind where - fromJSON (JNumber 1) = pure Text - fromJSON (JNumber 2) = pure Method - fromJSON (JNumber 3) = pure Function - fromJSON (JNumber 4) = pure Constructor - fromJSON (JNumber 5) = pure Field - fromJSON (JNumber 6) = pure Variable - fromJSON (JNumber 7) = pure Class - fromJSON (JNumber 8) = pure Interface - fromJSON (JNumber 9) = pure Module - fromJSON (JNumber 10) = pure Property - fromJSON (JNumber 11) = pure Unit_ - fromJSON (JNumber 12) = pure Value - fromJSON (JNumber 13) = pure Enum - fromJSON (JNumber 14) = pure Keyword - fromJSON (JNumber 15) = pure Snippet - fromJSON (JNumber 16) = pure Color - fromJSON (JNumber 17) = pure File - fromJSON (JNumber 18) = pure Reference - fromJSON (JNumber 19) = pure Folder - fromJSON (JNumber 20) = pure EnumMember - fromJSON (JNumber 21) = pure Constant - fromJSON (JNumber 22) = pure Struct - fromJSON (JNumber 23) = pure Event - fromJSON (JNumber 24) = pure Operator - fromJSON (JNumber 25) = pure TypeParameter - fromJSON _ = neutral - -namespace CompletionItemTag - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - data CompletionItemTag = Deprecated - -export -ToJSON CompletionItemTag where - toJSON Deprecated = JNumber 1 - -export -FromJSON CompletionItemTag where - fromJSON (JNumber 1) = pure Deprecated - fromJSON _ = neutral - -namespace InsertTextMode - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - data InsertTextMode = AsIs | AdjustIndentation - -export -ToJSON InsertTextMode where - toJSON AsIs = JNumber 1 - toJSON AdjustIndentation = JNumber 2 - -export -FromJSON InsertTextMode where - fromJSON (JNumber 1) = pure AsIs - fromJSON (JNumber 2) = pure AdjustIndentation - fromJSON _ = neutral - -namespace InsertTextFormat - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - data InsertTextFormat = PlainText | Snippet - -export -ToJSON InsertTextFormat where - toJSON PlainText = JNumber 1 - toJSON Snippet = JNumber 2 - -export -FromJSON InsertTextFormat where - fromJSON (JNumber 1) = pure PlainText - fromJSON (JNumber 2) = pure Snippet - fromJSON _ = neutral - -namespace CompletionItemClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - record CompletionItemTagSupportClientCapabilities where - constructor MkCompletionItemTagSupportClientCapabilities - valueSet : List CompletionItemTag - %runElab deriveJSON defaultOpts `{CompletionItemTagSupportClientCapabilities} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - record CompletionItemResolveSupportClientCapabilities where - constructor MkCompletionItemResolveSupportClientCapabilities - properties : List String - %runElab deriveJSON defaultOpts `{CompletionItemResolveSupportClientCapabilities} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - record InsertTextModeSupport where - constructor MkInsertTextModeSupport - valueSet : List InsertTextMode - %runElab deriveJSON defaultOpts `{InsertTextModeSupport} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - record CompletionItemClientCapabilities where - constructor MkCompletionItemClientCapabilities - snippetSupport : Maybe Bool - commitCharactersSupport : Maybe Bool - documentationFormat : Maybe (List MarkupKind) - deprecatedSupport : Maybe Bool - preselectSupport : Maybe Bool - tagSupport : Maybe CompletionItemTagSupportClientCapabilities - insertReplaceSupport : Maybe Bool - resolveSupport : Maybe CompletionItemResolveSupportClientCapabilities - insertTextModeSupport : Maybe InsertTextModeSupport - %runElab deriveJSON defaultOpts `{CompletionItemClientCapabilities} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - record CompletionItemKindClientCapabilities where - constructor MkCompletionItemKindClientCapabilities - valueSet : Maybe (List CompletionItemKind) - %runElab deriveJSON defaultOpts `{CompletionItemKindClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record CompletionClientCapabilities where - constructor MkCompletionClientCapabilities - dynamicRegistration : Maybe Bool - completionItem : Maybe CompletionItemClientCapabilities - completionItemKind : Maybe CompletionItemKindClientCapabilities - contextSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{CompletionClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record CompletionOptions where - constructor MkCompletionOptions - workDoneProgress : Maybe Bool - triggerCharacters : Maybe (List Char) - allCommitCharacters : Maybe (List Char) - resolveProvider : Maybe Bool -%runElab deriveJSON defaultOpts `{CompletionOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record CompletionRegistrationOptions where - constructor MkCompletionRegistrationOptions - documentSelector : (OneOf [DocumentSelector, Null]) - workDoneProgress : Maybe Bool - triggerCharacters : Maybe (List Char) - allCommitCharacters : Maybe (List Char) - resolveProvider : Maybe Bool -%runElab deriveJSON defaultOpts `{CompletionRegistrationOptions} - -namespace CompletionTriggerKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion - public export - data CompletionTriggerKind = Invoked | TriggerCharacter | TriggerForIncompleteCompletions - -export -ToJSON CompletionTriggerKind where - toJSON Invoked = JNumber 1 - toJSON TriggerCharacter = JNumber 2 - toJSON TriggerForIncompleteCompletions = JNumber 3 - -export -FromJSON CompletionTriggerKind where - fromJSON (JNumber 1) = pure Invoked - fromJSON (JNumber 2) = pure TriggerCharacter - fromJSON (JNumber 3) = pure TriggerForIncompleteCompletions - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record CompletionContext where - constructor MkCompletionContext - triggerKind : CompletionTriggerKind - triggerCharacter : Maybe String -%runElab deriveJSON defaultOpts `{CompletionContext} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record CompletionParams where - constructor MkCompletionParams - textDocument : TextDocumentIdentifier - position : Position - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - context : Maybe CompletionContext -%runElab deriveJSON defaultOpts `{CompletionParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record CompletionItem where - constructor MkCompletionItem - label : String - kind : Maybe CompletionItemKind - tags : Maybe (List CompletionItemTag) - detail : Maybe String - documentation : Maybe (OneOf [String, MarkupContent]) - deprecated : Maybe Bool - preselect : Maybe Bool - sortText : Maybe String - filterText : Maybe String - insertText : Maybe String - insertTextFormat : Maybe InsertTextFormat - insertTextMode : Maybe InsertTextMode - textEdit : Maybe (OneOf [TextEdit, InsertReplaceEdit]) - additionalTextEdits : Maybe (List TextEdit) - commitCharacters : Maybe (List Char) - command : Maybe Command - data_ : Maybe JSON -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CompletionItem} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record CompletionList where - constructor MkCompletionList - isIncomplete : Bool - items : List CompletionItem -%runElab deriveJSON defaultOpts `{CompletionList} diff --git a/src/Language/LSP/Message/Declaration.idr b/src/Language/LSP/Message/Declaration.idr deleted file mode 100644 index 1441cb5..0000000 --- a/src/Language/LSP/Message/Declaration.idr +++ /dev/null @@ -1,46 +0,0 @@ -module Language.LSP.Message.Declaration - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration -public export -record DeclarationClientCapabilities where - constructor MkDeclarationClientCapabilities - dynamicRegistration : Maybe Bool - linkSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{DeclarationClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration -public export -record DeclarationOptions where - constructor MkDeclarationOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{DeclarationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration -public export -record DeclarationRegistrationOptions where - constructor MkDeclarationRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe String -%runElab deriveJSON defaultOpts `{DeclarationRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration -public export -record DeclarationParams where - constructor MkDeclarationParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{DeclarationParams} diff --git a/src/Language/LSP/Message/Definition.idr b/src/Language/LSP/Message/Definition.idr deleted file mode 100644 index 6940bf3..0000000 --- a/src/Language/LSP/Message/Definition.idr +++ /dev/null @@ -1,79 +0,0 @@ -module Language.LSP.Message.Definition - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition -public export -record DefinitionClientCapabilities where - constructor MkDefinitionClientCapabilities - dynamicRegistration : Maybe Bool - linkSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{DefinitionClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition -public export -record DefinitionOptions where - constructor MkDefinitionOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{DefinitionOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition -public export -record DefinitionRegistrationOptions where - constructor MkDefinitionRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{DefinitionRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition -public export -record DefinitionParams where - constructor MkDefinitionParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{DefinitionParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition -public export -record TypeDefinitionClientCapabilities where - constructor MkTypeDefinitionClientCapabilities - dynamicRegistration : Maybe Bool - linkSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{TypeDefinitionClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition -public export -record TypeDefinitionOptions where - constructor MkTypeDefinitionOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{TypeDefinitionOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition -public export -record TypeDefinitionRegistrationOptions where - constructor MkTypeDefinitionRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe String -%runElab deriveJSON defaultOpts `{TypeDefinitionRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition -public export -record TypeDefinitionParams where - constructor MkTypeDefinitionParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{TypeDefinitionParams} diff --git a/src/Language/LSP/Message/Derive.idr b/src/Language/LSP/Message/Derive.idr deleted file mode 100644 index 08e84c8..0000000 --- a/src/Language/LSP/Message/Derive.idr +++ /dev/null @@ -1,211 +0,0 @@ -||| Automatic deriviation of JSON conversion interfaces. -||| -||| (C) The Idris Community, 2021 -module Language.LSP.Message.Derive - --- NOTE: Elaborator functions are evaluated as if they are defined inside the --- call location module, thus imported functions used inside elaborator --- functions should be exported publicly or explicitly imported at call --- location. -import public Data.Maybe -import public Data.SortedMap -import Data.String -import Language.JSON -import public Language.JSON.Interfaces -import Language.Reflection - -%language ElabReflection -%default total - -||| Options for automatic derivation of `ToJSON`/`FromJSON` instances. -public export -record JSONDeriveOpts where - constructor MkOpts - ||| If tagged, values are converted to JSON object with one field where the - ||| key is the name of the constructor and the value is the object obtained - ||| from converting the arguments of the constructor. - tagged : Bool - ||| Renaming rules for arguments where the name of the argument does not - ||| match the correspondent key in the translated JSON object. - renames : List (String, String) - ||| Fields that must be present in the JSON translation but have static - ||| values. - staticFields : List (String, JSON) - -public export -defaultOpts : JSONDeriveOpts -defaultOpts = MkOpts False [] [] - -stripNs : Name -> Name -stripNs (NS _ x) = x -stripNs x = x - -covering -genReadableSym : String -> Elab Name -genReadableSym hint = do - MN v i <- genSym hint - | _ => fail "cannot generate readable argument name" - pure $ UN $ Basic (v ++ show i) - -var : Name -> TTImp -var = IVar EmptyFC - -bindvar : String -> TTImp -bindvar = IBindVar EmptyFC - -primStr : String -> TTImp -primStr = IPrimVal EmptyFC . Str - -patClause : TTImp -> TTImp -> Clause -patClause = PatClause EmptyFC - -implicit' : TTImp -implicit' = Implicit EmptyFC True - --- TODO: add support for polymorphic types and maybe use another type for --- optional fields in place of Maybe. -||| Automatic derivation of `ToJSON` instances. -||| NOTE: all the fields in each constructor MUST be named, record already -||| comply but types declared with data must have constructors declared like -||| this: -||| ```idris example -||| data Position : Type where -||| MkPosition : (x : Integer) -> (y : Integer) -> Position -||| ``` -||| If the tagging option is enabled, types with multiple constructors are -||| translated to a JSON object with a single key-value pair where the key is -||| constructor name (without the namespace) and the value is the JSON object -||| translated as if untagged. -||| Constructor arguments that are `Maybe` instances are omitted if `Nothing` -||| and converted without the constructor if `Just`. If you need to translate a -||| mandatory field that can be nullable use the `Null` type. -||| -||| @ opts The automatic derivation options. -||| @ name The name of the type to derive for. Can be without namespace if unambigous. -public export covering -deriveToJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab () -deriveToJSON opts n = do - [(name, imp)] <- getType n - | xs => fail $ show n ++ " must be in scope and unique. Possible referred types are: " ++ show (fst <$> xs) - -- FIXME: temporary name for debugging, should be converted to a name impossible to define from users - -- and should not be exported, unless a specific option is enabled. - let funName = UN $ Basic ("toJSON" ++ show (stripNs n)) - let objName = UN $ Basic ("__impl_toJSON" ++ show (stripNs n)) - conNames <- getCons name - cons <- for conNames $ \n => do - [(conName, conImpl)] <- getType n - | _ => fail $ show n ++ " constructor must be in scope and unique" - (bindNames, rhs) <- genRHS conImpl - let rhs = if opts.tagged - then `(JObject $ [MkPair ~(primStr $ show $ stripNs n) (JObject $ catMaybes ~rhs)]) - else `(JObject $ catMaybes ~rhs) - let lhs = `(~(var funName) ~(applyBinds (var conName) (reverse bindNames))) - pure $ patClause lhs rhs - let funclaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(~(var name) -> JSON)) - let fundecl = IDef EmptyFC funName cons - declare [funclaim, fundecl] - [(ifName, _)] <- getType `{ToJSON} - | _ => fail "ToJSON interface must be in scope and unique" - [NS _ (DN _ ifCon)] <- getCons ifName - | _ => fail "Interface constructor error" - let retty = `(ToJSON ~(var name)) - let objclaim = IClaim EmptyFC MW Export [Hint True, Inline] (MkTy EmptyFC EmptyFC objName retty) - let objrhs = `(~(var ifCon) ~(var funName)) - let objdecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)] - declare [objclaim, objdecl] - where - genRHS : TTImp -> Elab (List Name, TTImp) - genRHS (IPi _ _ _ (Just n) `(Prelude.Types.Maybe ~argTy) retTy) = do - (ns, rest) <- genRHS retTy - let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames - pure (n :: ns, `(((MkPair ~name . toJSON) <$> ~(var n)) :: ~rest)) - genRHS (IPi _ _ _ (Just n) argTy retTy) = do - (ns, rest) <- genRHS retTy - let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames - pure (n :: ns, `(Just (MkPair ~name (toJSON ~(var n))) :: ~rest)) - genRHS (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named" - genRHS _ = do - -- Hack required, because if you quote directly opts.staticFields the elaborator introduces unsolved holes - r <- traverse (\(k, v) => (k,) <$> quote v) opts.staticFields - pure ([], foldr (\(k, v), acc => `(Just (MkPair ~(primStr k) ~v) :: ~acc)) `([]) r) - - applyBinds : TTImp -> List Name -> TTImp - applyBinds = foldr (\n, acc => `(~acc ~(bindvar $ show n))) - -||| Automatic derivation of `FromJSON` instances. -||| NOTE: all the fields in each constructor MUST be named, record already -||| comply but types declared with data must have constructors declared like -||| this: -||| ```idris example -||| data Position : Type where -||| MkPosition : (x : Integer) -> (y : Integer) -> Position -||| ``` -||| If the tagging option is enabled, types with multiple constructors are -||| translated to a JSON object with a single key-value pair where the key is -||| constructor name (without the namespace) and the value is the JSON object -||| translated as if untagged. -||| Constructor arguments that are `Maybe` instances are omitted if `Nothing` -||| and converted without the constructor if `Just`. If you need to translate a -||| mandatory field that can be nullable use the `Null` type. -||| -||| @ opts The automatic derivation options. -||| @ name The name of the type to derive for. Can be without namespace if unambigous. -public export covering -deriveFromJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab () -deriveFromJSON opts n = do - [(name, imp)] <- getType n - | xs => fail $ show n ++ " must be in scope and unique. Possible referred types are: " ++ show (fst <$> xs) - -- FIXME: temporary name for debugging, should be converted to a name impossible to define from users - -- and should not be exported, unless a specific option is enabled. - let funName = UN $ Basic ("fromJSON" ++ show (stripNs n)) - let objName = UN $ Basic ("__impl_fromJSON" ++ show (stripNs n)) - conNames <- getCons name - argName <- genReadableSym "arg" - cons <- for conNames $ \n => do - [(conName, conImpl)] <- getType n - | _ => fail $ show n ++ "constructor must be in scope and unique" - args <- getArgs conImpl - pure (conName, args) - clauses <- traverse (\(cn, as) => genClause funName cn argName (reverse as)) cons - let clauses = if opts.tagged - then (uncurry patClause <$> clauses) - else [patClause `(~(var funName) (JObject ~(bindvar $ show argName))) - (foldl (\acc, x => `(~x <|> ~acc)) `(Nothing) (snd <$> clauses))] - let funClaim = IClaim EmptyFC MW Export [Inline] (MkTy EmptyFC EmptyFC funName `(JSON -> Maybe ~(var name))) - let funDecl = IDef EmptyFC funName (clauses ++ [patClause `(~(var funName) ~implicit') `(Nothing)]) - declare [funClaim, funDecl] - [(ifName, _)] <- getType `{FromJSON} - | _ => fail "FromJSON interface must be in scope and unique" - [NS _ (DN _ ifCon)] <- getCons ifName - | _ => fail "Interface constructor error" - let retty = `(FromJSON ~(var name)) - let objClaim = IClaim EmptyFC MW Export [Hint True, Inline] (MkTy EmptyFC EmptyFC objName retty) - let objrhs = `(~(var ifCon) ~(var funName)) - let objDecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)] - declare [objClaim, objDecl] - where - getArgs : TTImp -> Elab (List (Name, TTImp)) - getArgs (IPi _ _ _ (Just n) argTy retTy) = ((n, argTy) ::) <$> getArgs retTy - getArgs (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named" - getArgs _ = pure [] - - genClause : Name -> Name -> Name -> List (Name, TTImp) -> Elab (TTImp, TTImp) - genClause funName t m xs = do - let lhs = `(~(var funName) (JObject [MkPair ~(primStr $ show $ stripNs t) (JObject ~(bindvar $ show m))])) - let rhs = foldr (\(n, type), acc => let name = primStr $ fromMaybe (show n) $ lookup (show n) opts.renames in - case type of - `(Prelude.Types.Maybe _) => `(~acc <*> (pure $ lookup ~name ~(var m) >>= fromJSON)) - _ => `(~acc <*> (lookup ~name ~(var m) >>= fromJSON))) - `(pure ~(var t)) xs - r <- traverse (\(k, v) => (k,) <$> quote v) opts.staticFields - let rhs = foldr (\(k, v), acc => `((lookup ~(primStr k) ~(var m) >>= (guard . (== ~v))) *> ~acc)) rhs r - pure (lhs, rhs) - -||| Automatic derivation of `ToJSON` and `FromJSON` instances. -||| See `deriveToJSON` and `deriveFromJSON`. -||| -||| @ opts The automatic derivation options. -||| @ name The name of the type to derive for. Can be without namespace if unambigous. -public export covering -deriveJSON : (opts : JSONDeriveOpts) -> (name : Name) -> Elab () -deriveJSON opts name = deriveToJSON opts name *> deriveFromJSON opts name diff --git a/src/Language/LSP/Message/Diagnostics.idr b/src/Language/LSP/Message/Diagnostics.idr deleted file mode 100644 index d391cb5..0000000 --- a/src/Language/LSP/Message/Diagnostics.idr +++ /dev/null @@ -1,105 +0,0 @@ -module Language.LSP.Message.Diagnostics - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -namespace DiagnosticTag - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic - public export - data DiagnosticTag = Unnecessary | Deprecated - -export -ToJSON DiagnosticTag where - toJSON Unnecessary = JNumber 1 - toJSON Deprecated = JNumber 2 - -export -FromJSON DiagnosticTag where - fromJSON (JNumber 1) = pure Unnecessary - fromJSON (JNumber 2) = pure Deprecated - fromJSON _ = neutral - -namespace DiagnosticSeverity - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic - public export - data DiagnosticSeverity = Error | Warning | Information | Hint - -export -ToJSON DiagnosticSeverity where - toJSON Error = JNumber 1 - toJSON Warning = JNumber 2 - toJSON Information = JNumber 3 - toJSON Hint = JNumber 4 - -export -FromJSON DiagnosticSeverity where - fromJSON (JNumber 1) = pure Error - fromJSON (JNumber 2) = pure Warning - fromJSON (JNumber 3) = pure Information - fromJSON (JNumber 4) = pure Hint - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic -public export -record DiagnosticRelatedInformation where - constructor MkDiagnosticRelatedInformation - location : Location - message : String -%runElab deriveJSON defaultOpts `{DiagnosticRelatedInformation} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic -public export -record CodeDescription where - constructor MkCodeDescription - href : URI -%runElab deriveJSON defaultOpts `{CodeDescription} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic -public export -record Diagnostic where - constructor MkDiagnostic - range : Range - severity : Maybe DiagnosticSeverity - code : Maybe (OneOf [Int, String]) - codeDescription : Maybe CodeDescription - source : Maybe String - message : String - tags : Maybe (List DiagnosticTag) - relatedInformation : Maybe (List DiagnosticRelatedInformation) - data_ : Maybe JSON -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{Diagnostic} - -namespace PublishDiagnosticsClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics - public export - record TagSupport where - constructor MkTagSupport - valueSet : List DiagnosticTag - %runElab deriveJSON defaultOpts `{TagSupport} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics -public export -record PublishDiagnosticsClientCapabilities where - constructor MkPublishDiagnosticsClientCapabilities - relatedInformation : Maybe Bool - tagSupport : Maybe TagSupport - versionSupport : Maybe Bool - codeDescriptionSupport : Maybe Bool - dataSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{PublishDiagnosticsClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics -public export -record PublishDiagnosticsParams where - constructor MkPublishDiagnosticsParams - uri : DocumentURI - version : Maybe Int - diagnostics : List Diagnostic -%runElab deriveJSON defaultOpts `{PublishDiagnosticsParams} diff --git a/src/Language/LSP/Message/DocumentColor.idr b/src/Language/LSP/Message/DocumentColor.idr deleted file mode 100644 index 4cff737..0000000 --- a/src/Language/LSP/Message/DocumentColor.idr +++ /dev/null @@ -1,82 +0,0 @@ -module Language.LSP.Message.DocumentColor - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.LSP.Message.Workspace -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor -public export -record DocumentColorClientCapabilities where - constructor MkDocumentColorClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentColorClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor -public export -record DocumentColorOptions where - constructor MkDocumentColorOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentColorOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor -public export -record DocumentColorRegistrationOptions where - constructor MkDocumentColorRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe String -%runElab deriveJSON defaultOpts `{DocumentColorRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor -public export -record DocumentColorParams where - constructor MkDocumentColorParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{DocumentColorParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor -public export -record Color where - constructor MkColor - red : Double - green : Double - blue : Double - alpha : Double -%runElab deriveJSON defaultOpts `{Color} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor -public export -record ColorInformation where - constructor MkColorInformation - range : Range - color : Color -%runElab deriveJSON defaultOpts `{ColorInformation} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_colorPresentation -public export -record ColorPresentationParams where - constructor MkColorPresentationParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - color : Color - range : Range -%runElab deriveJSON defaultOpts `{ColorPresentationParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_colorPresentation -public export -record ColorPresentation where - constructor MkColorPresentation - label : String - textEdit : Maybe TextEdit - additionalTextEdits : Maybe (List TextEdit) -%runElab deriveJSON defaultOpts `{ColorPresentation} diff --git a/src/Language/LSP/Message/DocumentFormatting.idr b/src/Language/LSP/Message/DocumentFormatting.idr deleted file mode 100644 index 3332853..0000000 --- a/src/Language/LSP/Message/DocumentFormatting.idr +++ /dev/null @@ -1,143 +0,0 @@ -module Language.LSP.Message.DocumentFormatting - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting -public export -record DocumentFormattingClientCapabilities where - constructor MkDocumentFormattingClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentFormattingClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting -public export -record DocumentFormattingOptions where - constructor MkDocumentFormattingOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentFormattingOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting -public export -record DocumentFormattingRegistrationOptions where - constructor MkDocumentFormattingRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{DocumentFormattingRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting -public export -record FormattingOptions where - constructor MkFormattingOptions - tabSize : Int - insertSpaces : Bool - trimTrailingWhitespace : Maybe Bool - insertFinalNewline : Maybe Bool - trimFinalNewlines : Maybe Bool - other : List (String, OneOf [Bool, Int, String]) - -export -ToJSON FormattingOptions where - toJSON opts = - JObject ((catMaybes [ Just ("tabSize", toJSON opts.tabSize) - , Just ("insertSpaces", toJSON opts.insertSpaces) - , ("trimTrailingWhitespace",) . toJSON <$> opts.trimTrailingWhitespace - , ("insertFinalNewline",) . toJSON <$> opts.insertFinalNewline - , ("trimFinalNewlines",) . toJSON <$> opts.trimFinalNewlines - ]) ++ (mapSnd toJSON <$> opts.other)) - -export -FromJSON FormattingOptions where - fromJSON (JObject arg) = - pure MkFormattingOptions <*> (lookup "tabSize" arg >>= fromJSON) - <*> (lookup "insertSpaces" arg >>= fromJSON) - <*> (pure $ lookup "trimTrailingWhitespace" arg >>= fromJSON) - <*> (pure $ lookup "insertFinalNewline" arg >>= fromJSON) - <*> (pure $ lookup "trimFinalNewlines" arg >>= fromJSON) - <*> (pure $ catMaybes $ map sequence $ map (mapSnd fromJSON) $ filter (\(k, _) => not $ k `elem` fields) $ toList arg) - where - fields : List String - fields = ["tabSize", "insertSpaces", "trimTrailingWhitespace", "insertFinalNewline", "trimFinalNewlines"] - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting -public export -record DocumentFormattingParams where - constructor MkDocumentFormattingParams - workDoneToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - options : FormattingOptions -%runElab deriveJSON defaultOpts `{DocumentFormattingParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting -public export -record DocumentRangeFormattingClientCapabilities where - constructor MkDocumentRangeFormattingClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentRangeFormattingClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting -public export -record DocumentRangeFormattingOptions where - constructor MkDocumentRangeFormattingOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentRangeFormattingOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting -public export -record DocumentRangeFormattingRegistrationOptions where - constructor MkDocumentRangeFormattingRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{DocumentRangeFormattingRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting -public export -record DocumentRangeFormattingParams where - constructor MkDocumentRangeFormattingParams - workDoneToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - range : Range - options : FormattingOptions -%runElab deriveJSON defaultOpts `{DocumentRangeFormattingParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting -public export -record DocumentOnTypeFormattingClientCapabilities where - constructor MkDocumentOnTypeFormattingClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting -public export -record DocumentOnTypeFormattingOptions where - constructor MkDocumentOnTypeFormattingOptions - firstTriggerCharacter : Char - moreTriggerCharacter : Maybe (List Char) -%runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting -public export -record DocumentOnTypeFormattingRegistrationOptions where - constructor MkDocumentOnTypeFormattingRegistrationOptions - firstTriggerCharacter : Char - moreTriggerCharacter : Maybe (List Char) - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting -public export -record DocumentOnTypeFormattingParams where - constructor MkDocumentOnTypeFormattingParams - textDocument : TextDocumentIdentifier - ch : Char - options : FormattingOptions -%runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingParams} diff --git a/src/Language/LSP/Message/DocumentHighlight.idr b/src/Language/LSP/Message/DocumentHighlight.idr deleted file mode 100644 index be42a80..0000000 --- a/src/Language/LSP/Message/DocumentHighlight.idr +++ /dev/null @@ -1,72 +0,0 @@ -module Language.LSP.Message.DocumentHighlight - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -public export -record DocumentHighlightClientCapabilities where - constructor MkDocumentHighlightClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentHighlightClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -public export -record DocumentHighlightOptions where - constructor MkDocumentHighlightOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentHighlightOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -public export -record DocumentHighlightRegistrationOptions where - constructor MkDocumentHighlightRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{DocumentHighlightRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -public export -record DocumentHighlightParams where - constructor MkDocumentHighlightParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{DocumentHighlightParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -namespace DocumentHighlightKind - public export - data DocumentHighlightKind = Text | Read | Write - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -export -ToJSON DocumentHighlightKind where - toJSON Text = JNumber 1 - toJSON Read = JNumber 2 - toJSON Write = JNumber 3 - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -export -FromJSON DocumentHighlightKind where - fromJSON (JNumber 1) = pure Text - fromJSON (JNumber 2) = pure Read - fromJSON (JNumber 3) = pure Write - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight -public export -record DocumentHighlight where - constructor MkDocumentHighlight - range : Range - kind : Maybe DocumentHighlightKind -%runElab deriveJSON defaultOpts `{DocumentHighlight} diff --git a/src/Language/LSP/Message/DocumentLink.idr b/src/Language/LSP/Message/DocumentLink.idr deleted file mode 100644 index 2475efa..0000000 --- a/src/Language/LSP/Message/DocumentLink.idr +++ /dev/null @@ -1,57 +0,0 @@ -module Language.LSP.Message.DocumentLink - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink -public export -record DocumentLinkClientCapabilities where - constructor MkDocumentLinkClientCapabilities - dynamicRegistration : Maybe Bool - tooltipSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentLinkClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink -public export -record DocumentLinkOptions where - constructor MkDocumentLinkOptions - workDoneProgress : Maybe Bool - resolveProvider : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentLinkOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink -public export -record DocumentLinkRegistrationOptions where - constructor MkDocumentLinkRegistrationOptions - workDoneProgress : Maybe Bool - resolveProvider : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{DocumentLinkRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink -public export -record DocumentLinkParams where - constructor MkDocumentLinkParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{DocumentLinkParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink -public export -record DocumentLink where - constructor MkDocumentLink - range : Range - target : Maybe DocumentURI - tooltip : Maybe String - data_ : Maybe JSON -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{DocumentLink} diff --git a/src/Language/LSP/Message/DocumentSymbols.idr b/src/Language/LSP/Message/DocumentSymbols.idr deleted file mode 100644 index c6a7440..0000000 --- a/src/Language/LSP/Message/DocumentSymbols.idr +++ /dev/null @@ -1,219 +0,0 @@ -module Language.LSP.Message.DocumentSymbols - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -namespace SymbolKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol - public export - data SymbolKind - = File - | Module - | Namespace - | Package - | Class - | Method - | Property - | Field - | Constructor - | Enum - | Interface - | Function - | Variable - | Constant - | String_ - | Number - | Boolean - | Array - | Object - | Key - | Null - | EnumMember - | Struct - | Event - | Operator - | TypeParameter - -export -ToJSON SymbolKind where - toJSON File = JNumber 1 - toJSON Module = JNumber 2 - toJSON Namespace = JNumber 3 - toJSON Package = JNumber 4 - toJSON Class = JNumber 5 - toJSON Method = JNumber 6 - toJSON Property = JNumber 7 - toJSON Field = JNumber 8 - toJSON Constructor = JNumber 9 - toJSON Enum = JNumber 10 - toJSON Interface = JNumber 11 - toJSON Function = JNumber 12 - toJSON Variable = JNumber 13 - toJSON Constant = JNumber 14 - toJSON String_ = JNumber 15 - toJSON Number = JNumber 16 - toJSON Boolean = JNumber 17 - toJSON Array = JNumber 18 - toJSON Object = JNumber 19 - toJSON Key = JNumber 20 - toJSON Null = JNumber 21 - toJSON EnumMember = JNumber 22 - toJSON Struct = JNumber 23 - toJSON Event = JNumber 24 - toJSON Operator = JNumber 25 - toJSON TypeParameter = JNumber 26 - -export -FromJSON SymbolKind where - fromJSON (JNumber 1) = pure File - fromJSON (JNumber 2) = pure Module - fromJSON (JNumber 3) = pure Namespace - fromJSON (JNumber 4) = pure Package - fromJSON (JNumber 5) = pure Class - fromJSON (JNumber 6) = pure Method - fromJSON (JNumber 7) = pure Property - fromJSON (JNumber 8) = pure Field - fromJSON (JNumber 9) = pure Constructor - fromJSON (JNumber 10) = pure Enum - fromJSON (JNumber 11) = pure Interface - fromJSON (JNumber 12) = pure Function - fromJSON (JNumber 13) = pure Variable - fromJSON (JNumber 14) = pure Constant - fromJSON (JNumber 15) = pure String_ - fromJSON (JNumber 16) = pure Number - fromJSON (JNumber 17) = pure Boolean - fromJSON (JNumber 18) = pure Array - fromJSON (JNumber 19) = pure Object - fromJSON (JNumber 20) = pure Key - fromJSON (JNumber 21) = pure Null - fromJSON (JNumber 22) = pure EnumMember - fromJSON (JNumber 23) = pure Struct - fromJSON (JNumber 24) = pure Event - fromJSON (JNumber 25) = pure Operator - fromJSON (JNumber 26) = pure TypeParameter - fromJSON _ = Nothing - -namespace SymbolTag - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol - public export - data SymbolTag = Deprecated - -export -ToJSON SymbolTag where - toJSON Deprecated = JNumber 1 - -export -FromJSON SymbolTag where - fromJSON (JNumber 1) = pure Deprecated - fromJSON _ = Nothing - -namespace DocumentSymbolClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol - public export - record DocumentSymbolKind where - constructor MkDocumentSymbolKind - valueSet : Maybe (List SymbolKind) - %runElab deriveJSON defaultOpts `{DocumentSymbolKind} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol - public export - record DocumentSymbolTag where - constructor MkDocumentSymbolTag - valueSet : Maybe (List SymbolTag) - %runElab deriveJSON defaultOpts `{DocumentSymbolTag} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol -public export -record DocumentSymbolClientCapabilities where - constructor MkDocumentSymbolClientCapabilities - dynamicRegistration : Maybe Bool - symbolKind : Maybe DocumentSymbolKind - hierarchicalDocumentSymbolSupport : Maybe Bool - tagSupport : Maybe DocumentSymbolTag - labelSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{DocumentSymbolClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol -public export -record DocumentSymbolOptions where - constructor MkDocumentSymbolOptions - workDoneProgress : Maybe Bool - label : Maybe String -%runElab deriveJSON defaultOpts `{DocumentSymbolOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol -public export -record DocumentSymbolRegistrationOptions where - constructor MkDocumentSymbolRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - label : Maybe String -%runElab deriveJSON defaultOpts `{DocumentSymbolRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol -public export -record DocumentSymbolParams where - constructor MkDocumentSymbolParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{DocumentSymbolParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol -public export -record DocumentSymbol where - constructor MkDocumentSymbol - name : String - detail : Maybe String - kind : SymbolKind - tags : Maybe (List SymbolTag) - deprecated : Maybe Bool - range : Range - selectionRange : Range - children : Maybe (List (Inf DocumentSymbol)) - -export -- FIXME?: Can I Avoid assert_total? Try indexing it with the depth -ToJSON DocumentSymbol where - toJSON (MkDocumentSymbol name detail kind tags deprecated range selectionRange children) = assert_total $ - JObject (catMaybes [ Just ("name", toJSON name) - , (MkPair "detail" . toJSON) <$> detail - , Just ("kind", toJSON kind) - , (MkPair "tags" . toJSON) <$> tags - , Just ("deprecated", toJSON deprecated) - , Just ("range", toJSON range) - , Just ("selectionRange", toJSON selectionRange) - , (MkPair "children" . toJSON) <$> children - ]) - -export covering -FromJSON DocumentSymbol where - fromJSON (JObject arg) = - pure MkDocumentSymbol <*> (lookup "name" arg >>= fromJSON) - <*> (pure $ lookup "detail" arg >>= fromJSON) - <*> (lookup "kind" arg >>= fromJSON) - <*> (pure $ lookup "tags" arg >>= fromJSON) - <*> (pure $ lookup "deprecated" arg >>= fromJSON) - <*> (lookup "range" arg >>= fromJSON) - <*> (lookup "selectionRange" arg >>= fromJSON) - <*> (pure $ lookup "children" arg >>= fromJSON) - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol -public export -record SymbolInformation where - constructor MkSymbolInformation - name : String - kind : SymbolKind - tags : Maybe (List SymbolTag) - deprecated : Maybe Bool - location : Location - containerName : Maybe String -%runElab deriveJSON defaultOpts `{SymbolInformation} diff --git a/src/Language/LSP/Message/FoldingRange.idr b/src/Language/LSP/Message/FoldingRange.idr deleted file mode 100644 index ea917f0..0000000 --- a/src/Language/LSP/Message/FoldingRange.idr +++ /dev/null @@ -1,74 +0,0 @@ -module Language.LSP.Message.FoldingRange - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange -public export -record FoldingRangeClientCapabilities where - constructor MkFoldingRangeClientCapabilities - dynamicRegistration : Maybe Bool - rangeLimit : Maybe Int - lineFoldingOnly : Maybe Bool -%runElab deriveJSON defaultOpts `{FoldingRangeClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange -public export -record FoldingRangeOptions where - constructor MkFoldingRangeOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{FoldingRangeOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange -public export -record FoldingRangeRegistrationOptions where - constructor MkFoldingRangeRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe String -%runElab deriveJSON defaultOpts `{FoldingRangeRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange -public export -record FoldingRangeParams where - constructor MkFoldingRangeParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{FoldingRangeParams} - -namespace FoldingRangeKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange - public export - data FoldingRangeKind = Comment | Imports | Region - -export -ToJSON FoldingRangeKind where - toJSON Comment = JString "comment" - toJSON Imports = JString "imports" - toJSON Region = JString "region" - -export -FromJSON FoldingRangeKind where - fromJSON (JString "comment") = pure Comment - fromJSON (JString "imports") = pure Imports - fromJSON (JString "region") = pure Region - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange -public export -record FoldingRange where - constructor MkFoldingRange - startLine : Int - startCharacter : Maybe Int - endLine : Int - endCharacter : Maybe Int - kind : Maybe String -%runElab deriveJSON defaultOpts `{FoldingRange} diff --git a/src/Language/LSP/Message/Hover.idr b/src/Language/LSP/Message/Hover.idr deleted file mode 100644 index ce367eb..0000000 --- a/src/Language/LSP/Message/Hover.idr +++ /dev/null @@ -1,53 +0,0 @@ -module Language.LSP.Message.Hover - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Markup -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover -public export -record HoverClientCapabilities where - constructor MkHoverClientCapabilities - dynamicRegistration : Maybe Bool - contentFormat : Maybe (List MarkupKind) -%runElab deriveJSON defaultOpts `{HoverClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover -public export -record HoverOptions where - constructor MkHoverOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{HoverOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover -public export -record HoverRegistrationOptions where - constructor MkHoverRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{HoverRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover -public export -record HoverParams where - constructor MkHoverParams - workDoneToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{HoverParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover -public export -record Hover where - constructor MkHover - contents : OneOf [MarkedString, List MarkedString, MarkupContent] - range : Maybe Range -%runElab deriveJSON defaultOpts `{Hover} diff --git a/src/Language/LSP/Message/Implementation.idr b/src/Language/LSP/Message/Implementation.idr deleted file mode 100644 index 3d4115f..0000000 --- a/src/Language/LSP/Message/Implementation.idr +++ /dev/null @@ -1,46 +0,0 @@ -module Language.LSP.Message.Implementation - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_implementation -public export -record ImplementationClientCapabilities where - constructor MkImplementationClientCapabilities - dynamicRegistration : Maybe Bool - linkSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{ImplementationClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_implementation -public export -record ImplementationOptions where - constructor MkImplementationOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{ImplementationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_implementation -public export -record ImplementationRegistrationOptions where - constructor MkImplementationRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe String -%runElab deriveJSON defaultOpts `{ImplementationRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_implementation -public export -record ImplementationParams where - constructor MkImplementationParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{ImplementationParams} diff --git a/src/Language/LSP/Message/Initialize.idr b/src/Language/LSP/Message/Initialize.idr deleted file mode 100644 index de3b04f..0000000 --- a/src/Language/LSP/Message/Initialize.idr +++ /dev/null @@ -1,60 +0,0 @@ -module Language.LSP.Message.Initialize - -import Language.JSON -import Language.LSP.Message.ClientCapabilities -import Language.LSP.Message.Derive -import Language.LSP.Message.Progress -import Language.LSP.Message.ServerCapabilities -import Language.LSP.Message.Trace -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.LSP.Message.Workspace -import Language.Reflection - -%language ElabReflection -%default total - -namespace InitializeParams - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize - public export - record ClientInfo where - name : String - version : Maybe String - %runElab deriveJSON defaultOpts `{ClientInfo} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record InitializeParams where - constructor MkInitializeParams - processId : OneOf [Integer, Null] - clientInfo : Maybe ClientInfo - locale : Maybe String - rootPath : Maybe (OneOf [String, Null]) - rootUri : OneOf [URI, Null] - initializationOptions : Maybe JSON - capabilities : ClientCapabilities - trace : Maybe Trace - workspaceFolders : Maybe (OneOf [List WorkspaceFolder, Null]) - workDoneToken : Maybe ProgressToken -%runElab deriveJSON defaultOpts `{InitializeParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record InitializeResult where - constructor MkInitializeResult - capabilities : ServerCapabilities - serverInfo : Maybe ServerInfo -%runElab deriveJSON defaultOpts `{InitializeResult} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record InitializeError where - constructor MkInitializeError - retry : Bool -%runElab deriveJSON defaultOpts `{InitializeError} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialized -public export -record InitializedParams where - constructor MkInitializedParams -%runElab deriveJSON defaultOpts `{InitializedParams} diff --git a/src/Language/LSP/Message/LinkedEditingRange.idr b/src/Language/LSP/Message/LinkedEditingRange.idr deleted file mode 100644 index 6b6f8b4..0000000 --- a/src/Language/LSP/Message/LinkedEditingRange.idr +++ /dev/null @@ -1,52 +0,0 @@ -module Language.LSP.Message.LinkedEditingRange - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange -public export -record LinkedEditingRangeClientCapabilities where - constructor MkLinkedEditingRangeClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{LinkedEditingRangeClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange -public export -record LinkedEditingRangeOptions where - constructor MkLinkedEditingRangesOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{LinkedEditingRangeOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange -public export -record LinkedEditingRangeRegistrationOptions where - constructor MkLinkedEditingRangesRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe Bool -%runElab deriveJSON defaultOpts `{LinkedEditingRangeRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange -public export -record LinkedEditingRangeParams where - constructor MkLinkedEditingRangesParams - workDoneToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{LinkedEditingRangeParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange -public export -record LinkedEditingRanges where - constructor MkLinkedEditingRanges - ranges : List Range - wordPattern : Maybe String -%runElab deriveJSON defaultOpts `{LinkedEditingRanges} diff --git a/src/Language/LSP/Message/Location.idr b/src/Language/LSP/Message/Location.idr deleted file mode 100644 index ba12ec2..0000000 --- a/src/Language/LSP/Message/Location.idr +++ /dev/null @@ -1,58 +0,0 @@ -module Language.LSP.Message.Location - -import Data.URI -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.Reflection - -%hide Prelude.Range -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#position -public export -record Position where - constructor MkPosition - line : Int - character : Int -%runElab deriveJSON defaultOpts `{Position} - -export -Eq Position where - (MkPosition line1 char1) == (MkPosition line2 char2) = line1 == line2 && char1 == char2 - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#range -public export -record Range where - constructor MkRange - start : Position - end : Position -%runElab deriveJSON defaultOpts `{Range} - -export -Eq Range where - (MkRange start1 end1) == (MkRange start2 end2) = start1 == start2 && end1 == end2 - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#location -public export -record Location where - constructor MkLocation - uri : URI - range : Range -%runElab deriveJSON defaultOpts `{Location} - -export -Eq Location where - (MkLocation uri1 range1) == (MkLocation uri2 range2) = uri1 == uri2 && range1 == range2 - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#locationLink -public export -record LocationLink where - constructor MkLocationLink - originSelectionRange : Maybe Range - targetUri : URI - targetRange : Range - targetSelectionRange : Range -%runElab deriveJSON defaultOpts `{LocationLink} diff --git a/src/Language/LSP/Message/Markup.idr b/src/Language/LSP/Message/Markup.idr deleted file mode 100644 index 8f92023..0000000 --- a/src/Language/LSP/Message/Markup.idr +++ /dev/null @@ -1,62 +0,0 @@ -module Language.LSP.Message.Markup - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -namespace MarkupKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent - public export - data MarkupKind = PlainText | Markdown - -public export -Eq MarkupKind where - PlainText == PlainText = True - PlainText == _ = False - Markdown == Markdown = True - Markdown == _ = False - -export -ToJSON MarkupKind where - toJSON PlainText = JString "plaintext" - toJSON Markdown = JString "markdown" - -export -FromJSON MarkupKind where - fromJSON (JString "plaintext") = pure PlainText - fromJSON (JString "markdown") = pure Markdown - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent -public export -record MarkupContent where - constructor MkMarkupContent - kind : MarkupKind - value : String -%runElab deriveJSON defaultOpts `{MarkupContent} - -namespace MarkedString - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover - public export - record MarkedStringWithLanguage where - constructor MkMarkedStringWithLanguage - language : String - value : String - %runElab deriveJSON defaultOpts `{MarkedStringWithLanguage} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover -public export -MarkedString : Type -MarkedString = OneOf [String, MarkedStringWithLanguage] - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent -public export -record MarkdownClientCapabilities where - constructor MkMarkdownClientCapabilities - parser : String - version : Maybe String -%runElab deriveJSON defaultOpts `{MarkdownClientCapabilities} diff --git a/src/Language/LSP/Message/Message.idr b/src/Language/LSP/Message/Message.idr deleted file mode 100644 index ac5e9fd..0000000 --- a/src/Language/LSP/Message/Message.idr +++ /dev/null @@ -1,567 +0,0 @@ -||| Definitions of messages and associated payloads and responses. -||| -||| (C) The Idris Community, 2021 -module Language.LSP.Message.Message - -import Data.OneOf -import Language.JSON -import Language.LSP.Message.CallHierarchy -import Language.LSP.Message.Cancel -import Language.LSP.Message.CodeAction -import Language.LSP.Message.CodeLens -import Language.LSP.Message.Command -import Language.LSP.Message.Completion -import Language.LSP.Message.Declaration -import Language.LSP.Message.Definition -import Language.LSP.Message.Derive -import Language.LSP.Message.Diagnostics -import Language.LSP.Message.DocumentColor -import Language.LSP.Message.DocumentFormatting -import Language.LSP.Message.DocumentHighlight -import Language.LSP.Message.DocumentLink -import Language.LSP.Message.DocumentSymbols -import Language.LSP.Message.FoldingRange -import Language.LSP.Message.Hover -import Language.LSP.Message.Implementation -import Language.LSP.Message.Initialize -import Language.LSP.Message.LinkedEditingRange -import Language.LSP.Message.Location -import Language.LSP.Message.Method -import Language.LSP.Message.Moniker -import Language.LSP.Message.Progress -import Language.LSP.Message.References -import Language.LSP.Message.Registration -import Language.LSP.Message.Rename -import Language.LSP.Message.SelectionRange -import Language.LSP.Message.SemanticTokens -import Language.LSP.Message.SignatureHelp -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Trace -import Language.LSP.Message.Utils -import Language.LSP.Message.Window -import Language.LSP.Message.Workspace -import Language.Reflection - -%language ElabReflection -%default total - -||| Maps the parameters associated to each type of method. -public export -MessageParams : (method : Method from type) -> Type -MessageParams Initialize = InitializeParams -MessageParams Initialized = InitializedParams -MessageParams Shutdown = Maybe Null -MessageParams Exit = Maybe Null -MessageParams SetTrace = SetTraceParams -MessageParams WindowWorkDoneProgressCancel = WorkDoneProgressCancelParams -MessageParams WorkspaceDidChangeWorkspaceFolders = DidChangeWorkspaceFoldersParams -MessageParams WorkspaceDidChangeConfiguration = DidChangeConfigurationParams -MessageParams WorkspaceDidChangeWatchedFiles = DidChangeWatchedFilesParams -MessageParams WorkspaceSymbol = WorkspaceSymbolParams -MessageParams WorkspaceExecuteCommand = ExecuteCommandParams -MessageParams WorkspaceWillCreateFiles = CreateFilesParams -MessageParams TextDocumentDidOpen = DidOpenTextDocumentParams -MessageParams TextDocumentDidChange = DidChangeTextDocumentParams -MessageParams TextDocumentWillSave = WillSaveTextDocumentParams -MessageParams TextDocumentWillSaveWaitUntil = WillSaveTextDocumentParams -MessageParams TextDocumentDidSave = DidSaveTextDocumentParams -MessageParams TextDocumentDidClose = DidCloseTextDocumentParams -MessageParams CompletionItemResolve = CompletionItem -MessageParams TextDocumentHover = HoverParams -MessageParams TextDocumentSignatureHelp = SignatureHelpParams -MessageParams TextDocumentDeclaration = DeclarationParams -MessageParams TextDocumentDefinition = DefinitionParams -MessageParams TextDocumentTypeDefinition = TypeDefinitionParams -MessageParams TextDocumentImplementation = ImplementationParams -MessageParams TextDocumentReferences = ReferenceParams -MessageParams TextDocumentDocumentHighlight = DocumentHighlightParams -MessageParams TextDocumentDocumentSymbol = DocumentSymbolParams -MessageParams TextDocumentCodeAction = CodeActionParams -MessageParams CodeActionResolve = CodeAction -MessageParams TextDocumentCodeLens = CodeLensParams -MessageParams CodeLensResolve = CodeLens -MessageParams TextDocumentDocumentLink = DocumentLinkParams -MessageParams DocumentLinkResolve = DocumentLink -MessageParams TextDocumentDocumentColor = DocumentColorParams -MessageParams TextDocumentFormatting = DocumentFormattingParams -MessageParams TextDocumentRangeFormatting = DocumentRangeFormattingParams -MessageParams TextDocumentOnTypeFormatting = DocumentOnTypeFormattingParams -MessageParams TextDocumentRename = RenameParams -MessageParams TextDocumentPrepareRename = PrepareRenameParams -MessageParams TextDocumentFoldingRange = FoldingRangeParams -MessageParams TextDocumentSelectionRange = SelectionRangeParams -MessageParams TextDocumentPrepareCallHierarchy = CallHierarchyParams -MessageParams CallHierarchyIncomingCalls = CallHierarchyIncomingCallsParams -MessageParams CallHierarchyOutgoingCalls = CallHierarchyOutgoingCallsParams -MessageParams TextDocumentSemanticTokensFull = SemanticTokensParams -MessageParams TextDocumentSemanticTokensFullDelta = SemanticTokensDeltaParams -MessageParams TextDocumentSemanticTokensRange = SemanticTokensRangeParams -MessageParams WorkspaceSemanticTokensRefresh = Maybe Null -MessageParams TextDocumentLinkedEditingRange = LinkedEditingRangeParams -MessageParams TextDocumentMoniker = MonikerParams -MessageParams LogTrace = LogTraceParams -MessageParams WindowShowMessage = ShowMessageParams -MessageParams WindowShowMessageRequest = ShowMessageRequestParams -MessageParams WindowShowDocument = ShowDocumentParams -MessageParams WindowLogMessage = LogMessageParams -MessageParams WindowWorkDoneProgressCreate = WorkDoneProgressCreateParams -MessageParams TelemetryEvent = JSON -MessageParams ClientRegisterCapability = RegistrationParams -MessageParams ClientUnregisterCapability = UnregistrationParams -MessageParams WorkspaceWorkspaceFolders = Maybe Null -MessageParams WorkspaceConfiguration = ConfigurationParams -MessageParams WorkspaceApplyEdit = ApplyWorkspaceEditParams -MessageParams TextDocumentPublishDiagnostics = PublishDiagnosticsParams -MessageParams TextDocumentCompletion = CompletionParams -MessageParams WorkspaceCodeLensRefresh = Maybe Null -MessageParams CancelRequest = CancelParams -MessageParams Progress = OneOf [WorkDoneProgressBegin, WorkDoneProgressReport, WorkDoneProgressEnd] - --- Hacky, but avoids having to carry a FromJSON (MessageParams method) inside sigma types -findParamsImpl : (method : Method from type) -> FromJSON (MessageParams method) -findParamsImpl Initialize = %search -findParamsImpl Initialized = %search -findParamsImpl Shutdown = %search -findParamsImpl Exit = %search -findParamsImpl SetTrace = %search -findParamsImpl WindowWorkDoneProgressCancel = %search -findParamsImpl WorkspaceDidChangeWorkspaceFolders = %search -findParamsImpl WorkspaceDidChangeConfiguration = %search -findParamsImpl WorkspaceDidChangeWatchedFiles = %search -findParamsImpl WorkspaceSymbol = %search -findParamsImpl WorkspaceExecuteCommand = %search -findParamsImpl WorkspaceWillCreateFiles = %search -findParamsImpl TextDocumentDidOpen = %search -findParamsImpl TextDocumentDidChange = %search -findParamsImpl TextDocumentWillSave = %search -findParamsImpl TextDocumentWillSaveWaitUntil = %search -findParamsImpl TextDocumentDidSave = %search -findParamsImpl TextDocumentDidClose = %search -findParamsImpl CompletionItemResolve = %search -findParamsImpl TextDocumentHover = %search -findParamsImpl TextDocumentSignatureHelp = %search -findParamsImpl TextDocumentDeclaration = %search -findParamsImpl TextDocumentDefinition = %search -findParamsImpl TextDocumentTypeDefinition = %search -findParamsImpl TextDocumentImplementation = %search -findParamsImpl TextDocumentReferences = %search -findParamsImpl TextDocumentDocumentHighlight = %search -findParamsImpl TextDocumentDocumentSymbol = %search -findParamsImpl TextDocumentCodeAction = %search -findParamsImpl CodeActionResolve = %search -findParamsImpl TextDocumentCodeLens = %search -findParamsImpl CodeLensResolve = %search -findParamsImpl TextDocumentDocumentLink = %search -findParamsImpl DocumentLinkResolve = %search -findParamsImpl TextDocumentDocumentColor = %search -findParamsImpl TextDocumentFormatting = %search -findParamsImpl TextDocumentRangeFormatting = %search -findParamsImpl TextDocumentOnTypeFormatting = %search -findParamsImpl TextDocumentRename = %search -findParamsImpl TextDocumentPrepareRename = %search -findParamsImpl TextDocumentFoldingRange = %search -findParamsImpl TextDocumentSelectionRange = %search -findParamsImpl TextDocumentPrepareCallHierarchy = %search -findParamsImpl CallHierarchyIncomingCalls = %search -findParamsImpl CallHierarchyOutgoingCalls = %search -findParamsImpl TextDocumentSemanticTokensFull = %search -findParamsImpl TextDocumentSemanticTokensFullDelta = %search -findParamsImpl TextDocumentSemanticTokensRange = %search -findParamsImpl WorkspaceSemanticTokensRefresh = %search -findParamsImpl TextDocumentLinkedEditingRange = %search -findParamsImpl TextDocumentMoniker = %search -findParamsImpl LogTrace = %search -findParamsImpl WindowShowMessage = %search -findParamsImpl WindowShowMessageRequest = %search -findParamsImpl WindowShowDocument = %search -findParamsImpl WindowLogMessage = %search -findParamsImpl WindowWorkDoneProgressCreate = %search -findParamsImpl TelemetryEvent = %search -findParamsImpl ClientRegisterCapability = %search -findParamsImpl ClientUnregisterCapability = %search -findParamsImpl WorkspaceWorkspaceFolders = %search -findParamsImpl WorkspaceConfiguration = %search -findParamsImpl WorkspaceApplyEdit = %search -findParamsImpl TextDocumentPublishDiagnostics = %search -findParamsImpl TextDocumentCompletion = %search -findParamsImpl WorkspaceCodeLensRefresh = %search -findParamsImpl CancelRequest = %search -findParamsImpl Progress = %search - -||| Maps the response associated to each type of method. -public export -ResponseResult : (method : Method from Request) -> Type -ResponseResult Initialize = InitializeResult -ResponseResult Shutdown = Maybe Null -ResponseResult WorkspaceSymbol = OneOf [List SymbolInformation, Null] -ResponseResult WorkspaceExecuteCommand = JSON -ResponseResult WorkspaceWillCreateFiles = OneOf [WorkspaceEdit, Null] -ResponseResult TextDocumentWillSaveWaitUntil = OneOf [List TextEdit, Null] -ResponseResult CompletionItemResolve = CompletionItem -ResponseResult TextDocumentHover = OneOf [Hover, Null] -ResponseResult TextDocumentSignatureHelp = OneOf [SignatureHelp, Null] -ResponseResult TextDocumentDeclaration = OneOf [Location, List Location, List LocationLink, Null] -ResponseResult TextDocumentDefinition = OneOf [Location, List Location, List LocationLink, Null] -ResponseResult TextDocumentTypeDefinition = OneOf [Location, List Location, List LocationLink, Null] -ResponseResult TextDocumentImplementation = OneOf [Location, List Location, List LocationLink, Null] -ResponseResult TextDocumentReferences = OneOf [List Location, Null] -ResponseResult TextDocumentDocumentHighlight = OneOf [List DocumentHighlight, Null] -ResponseResult TextDocumentDocumentSymbol = OneOf [List DocumentSymbol, List SymbolInformation, Null] -ResponseResult TextDocumentCodeAction = OneOf [List (OneOf [Command, CodeAction]), Null] -ResponseResult CodeActionResolve = CodeAction -ResponseResult TextDocumentCodeLens = OneOf [List CodeLens, Null] -ResponseResult CodeLensResolve = Maybe Null -ResponseResult TextDocumentDocumentLink = OneOf [List DocumentLink, Null] -ResponseResult DocumentLinkResolve = DocumentLink -ResponseResult TextDocumentDocumentColor = List ColorInformation -ResponseResult TextDocumentFormatting = OneOf [List TextEdit, Null] -ResponseResult TextDocumentRangeFormatting = OneOf [List TextEdit, Null] -ResponseResult TextDocumentOnTypeFormatting = OneOf [List TextEdit, Null] -ResponseResult TextDocumentRename = OneOf [WorkspaceEdit, Null] -ResponseResult TextDocumentPrepareRename = OneOf [Range, PrepareRenamePlaceholderResponse, PrepareRenameDefaultResponse, Null] -ResponseResult TextDocumentFoldingRange = OneOf [List FoldingRange, Null] -ResponseResult TextDocumentSelectionRange = OneOf [List SelectionRange, Null] -ResponseResult TextDocumentPrepareCallHierarchy = OneOf [List CallHierarchyItem, Null] -ResponseResult CallHierarchyIncomingCalls = OneOf [List CallHierarchyIncomingCall, Null] -ResponseResult CallHierarchyOutgoingCalls = OneOf [List CallHierarchyOutgoingCall, Null] -ResponseResult TextDocumentSemanticTokensFull = OneOf [SemanticTokens, Null] -ResponseResult TextDocumentSemanticTokensFullDelta = OneOf [SemanticTokens, SemanticTokensDelta, Null] -ResponseResult TextDocumentSemanticTokensRange = OneOf [SemanticTokens, Null] -ResponseResult WorkspaceSemanticTokensRefresh = Maybe Null -ResponseResult TextDocumentLinkedEditingRange = OneOf [LinkedEditingRanges, Null] -ResponseResult TextDocumentMoniker = OneOf [List Moniker, Null] -ResponseResult WindowShowMessageRequest = OneOf [MessageActionItem, Null] -ResponseResult WindowShowDocument = ShowDocumentResult -ResponseResult WindowWorkDoneProgressCreate = Maybe Null -ResponseResult ClientRegisterCapability = Maybe Null -ResponseResult ClientUnregisterCapability = Maybe Null -ResponseResult WorkspaceWorkspaceFolders = OneOf [List WorkspaceFolder, Null] -ResponseResult WorkspaceConfiguration = List JSON -ResponseResult WorkspaceApplyEdit = ApplyWorkspaceEditResponse -ResponseResult TextDocumentCompletion = OneOf [List CompletionItem, CompletionList, Null] -ResponseResult WorkspaceCodeLensRefresh = Maybe Null - -findNotificationImpl : (method : Method from Notification) -> ToJSON (MessageParams method) -findNotificationImpl Initialized = %search -findNotificationImpl Exit = %search -findNotificationImpl SetTrace = %search -findNotificationImpl WindowWorkDoneProgressCancel = %search -findNotificationImpl WorkspaceDidChangeWorkspaceFolders = %search -findNotificationImpl WorkspaceDidChangeConfiguration = %search -findNotificationImpl WorkspaceDidChangeWatchedFiles = %search -findNotificationImpl TextDocumentDidOpen = %search -findNotificationImpl TextDocumentDidChange = %search -findNotificationImpl TextDocumentWillSave = %search -findNotificationImpl TextDocumentDidSave = %search -findNotificationImpl TextDocumentDidClose = %search -findNotificationImpl LogTrace = %search -findNotificationImpl WindowShowMessage = %search -findNotificationImpl WindowLogMessage = %search -findNotificationImpl TelemetryEvent = %search -findNotificationImpl TextDocumentPublishDiagnostics = %search -findNotificationImpl CancelRequest = %search -findNotificationImpl Progress = %search - -findRequestImpl : (method : Method from Request) -> ToJSON (MessageParams method) -findRequestImpl Initialize = %search -findRequestImpl Shutdown = %search -findRequestImpl WorkspaceSymbol = %search -findRequestImpl WorkspaceExecuteCommand = %search -findRequestImpl WorkspaceWillCreateFiles = %search -findRequestImpl TextDocumentWillSaveWaitUntil = %search -findRequestImpl CompletionItemResolve = %search -findRequestImpl TextDocumentHover = %search -findRequestImpl TextDocumentSignatureHelp = %search -findRequestImpl TextDocumentDeclaration = %search -findRequestImpl TextDocumentDefinition = %search -findRequestImpl TextDocumentTypeDefinition = %search -findRequestImpl TextDocumentImplementation = %search -findRequestImpl TextDocumentReferences = %search -findRequestImpl TextDocumentDocumentHighlight = %search -findRequestImpl TextDocumentDocumentSymbol = %search -findRequestImpl TextDocumentCodeAction = %search -findRequestImpl CodeActionResolve = %search -findRequestImpl TextDocumentCodeLens = %search -findRequestImpl CodeLensResolve = %search -findRequestImpl TextDocumentDocumentLink = %search -findRequestImpl DocumentLinkResolve = %search -findRequestImpl TextDocumentDocumentColor = %search -findRequestImpl TextDocumentFormatting = %search -findRequestImpl TextDocumentRangeFormatting = %search -findRequestImpl TextDocumentOnTypeFormatting = %search -findRequestImpl TextDocumentRename = %search -findRequestImpl TextDocumentPrepareRename = %search -findRequestImpl TextDocumentFoldingRange = %search -findRequestImpl TextDocumentSelectionRange = %search -findRequestImpl TextDocumentPrepareCallHierarchy = %search -findRequestImpl CallHierarchyIncomingCalls = %search -findRequestImpl CallHierarchyOutgoingCalls = %search -findRequestImpl TextDocumentSemanticTokensFull = %search -findRequestImpl TextDocumentSemanticTokensFullDelta = %search -findRequestImpl TextDocumentSemanticTokensRange = %search -findRequestImpl WorkspaceSemanticTokensRefresh = %search -findRequestImpl TextDocumentLinkedEditingRange = %search -findRequestImpl TextDocumentMoniker = %search -findRequestImpl WindowShowMessageRequest = %search -findRequestImpl WindowShowDocument = %search -findRequestImpl WindowWorkDoneProgressCreate = %search -findRequestImpl ClientRegisterCapability = %search -findRequestImpl ClientUnregisterCapability = %search -findRequestImpl WorkspaceWorkspaceFolders = %search -findRequestImpl WorkspaceConfiguration = %search -findRequestImpl WorkspaceApplyEdit = %search -findRequestImpl TextDocumentCompletion = %search -findRequestImpl WorkspaceCodeLensRefresh = %search - -findResultImpl : (method : Method from Request) -> ToJSON (ResponseResult method) -findResultImpl Initialize = %search -findResultImpl Shutdown = %search -findResultImpl WorkspaceSymbol = %search -findResultImpl WorkspaceExecuteCommand = %search -findResultImpl WorkspaceWillCreateFiles = %search -findResultImpl TextDocumentWillSaveWaitUntil = %search -findResultImpl CompletionItemResolve = %search -findResultImpl TextDocumentHover = %search -findResultImpl TextDocumentSignatureHelp = %search -findResultImpl TextDocumentDeclaration = %search -findResultImpl TextDocumentDefinition = %search -findResultImpl TextDocumentTypeDefinition = %search -findResultImpl TextDocumentImplementation = %search -findResultImpl TextDocumentReferences = %search -findResultImpl TextDocumentDocumentHighlight = %search -findResultImpl TextDocumentDocumentSymbol = %search -findResultImpl TextDocumentCodeAction = %search -findResultImpl CodeActionResolve = %search -findResultImpl TextDocumentCodeLens = %search -findResultImpl CodeLensResolve = %search -findResultImpl TextDocumentDocumentLink = %search -findResultImpl DocumentLinkResolve = %search -findResultImpl TextDocumentDocumentColor = %search -findResultImpl TextDocumentFormatting = %search -findResultImpl TextDocumentRangeFormatting = %search -findResultImpl TextDocumentOnTypeFormatting = %search -findResultImpl TextDocumentRename = %search -findResultImpl TextDocumentPrepareRename = %search -findResultImpl TextDocumentFoldingRange = %search -findResultImpl TextDocumentSelectionRange = %search -findResultImpl TextDocumentPrepareCallHierarchy = %search -findResultImpl CallHierarchyIncomingCalls = %search -findResultImpl CallHierarchyOutgoingCalls = %search -findResultImpl TextDocumentSemanticTokensFull = %search -findResultImpl TextDocumentSemanticTokensFullDelta = %search -findResultImpl TextDocumentSemanticTokensRange = %search -findResultImpl WorkspaceSemanticTokensRefresh = %search -findResultImpl TextDocumentLinkedEditingRange = %search -findResultImpl TextDocumentMoniker = %search -findResultImpl WindowShowMessageRequest = %search -findResultImpl WindowShowDocument = %search -findResultImpl WindowWorkDoneProgressCreate = %search -findResultImpl ClientRegisterCapability = %search -findResultImpl ClientUnregisterCapability = %search -findResultImpl WorkspaceWorkspaceFolders = %search -findResultImpl WorkspaceConfiguration = %search -findResultImpl WorkspaceApplyEdit = %search -findResultImpl TextDocumentCompletion = %search -findResultImpl WorkspaceCodeLensRefresh = %search - -||| Parse parameters -||| Since the params are sometimes optional we must parse Maybe JSON -||| TODO hacky replace with something better -export -fromMaybeJSONParameters : (method : Method from type) -> Maybe JSON -> Maybe (MessageParams method) -fromMaybeJSONParameters Exit arg = - pure $ join $ arg >>= (fromJSON @{findParamsImpl Exit}) -fromMaybeJSONParameters Shutdown arg = - pure $ join $ arg >>= (fromJSON @{findParamsImpl Shutdown}) -fromMaybeJSONParameters WorkspaceSemanticTokensRefresh arg = - pure $ join $ arg >>= (fromJSON @{findParamsImpl WorkspaceSemanticTokensRefresh}) -fromMaybeJSONParameters WorkspaceWorkspaceFolders arg = - pure $ join $ arg >>= (fromJSON @{findParamsImpl WorkspaceWorkspaceFolders}) -fromMaybeJSONParameters WorkspaceCodeLensRefresh arg = - pure $ join $ arg >>= (fromJSON @{findParamsImpl WorkspaceCodeLensRefresh}) -fromMaybeJSONParameters method arg = arg >>= (fromJSON @{findParamsImpl method}) - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#notificationMessage -public export -data NotificationMessage : Method from Notification -> Type where - MkNotificationMessage : (method : Method from Notification) - -> (params : MessageParams method) - -> NotificationMessage method - -export -{method : Method from Notification} -> ToJSON (NotificationMessage method) where - toJSON (MkNotificationMessage method params) = - JObject ([("jsonrpc", JString "2.0"), ("method", toJSON method), ("params", toJSON @{findNotificationImpl method} params)]) - -export -FromJSON (from ** method : Method from Notification ** NotificationMessage method) where - fromJSON (JObject arg) = do - lookup "jsonrpc" arg >>= (guard . (== JString "2.0")) - (from ** meth) <- lookup "method" arg >>= fromJSON {a = (from ** Method from Notification)} - case meth of - Exit => do let par = lookup "params" arg >>= (fromJSON @{findParamsImpl meth}) - pure (from ** meth ** MkNotificationMessage meth (join par)) - _ => do par <- lookup "params" arg >>= (fromJSON @{findParamsImpl meth}) - pure (from ** meth ** MkNotificationMessage meth par) - fromJSON _ = neutral - -namespace NotificationMessage - export - method : {0 m : Method from Notification} -> NotificationMessage m -> Method from Notification - method (MkNotificationMessage m _) = m - - export - params : {0 method : Method from Notification} -> NotificationMessage method -> MessageParams method - params (MkNotificationMessage _ p) = p - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#requestMessage -public export -data RequestMessage : Method from Request -> Type where - MkRequestMessage : (id : OneOf [Int, String]) - -> (method : Method from Request) - -> (params : MessageParams method) - -> RequestMessage method - -export -{method : Method from Request} -> ToJSON (RequestMessage method) where - toJSON (MkRequestMessage id method params) = - JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("method", toJSON method), ("params", toJSON @{findRequestImpl method} params)]) - -export -FromJSON (from ** method : Method from Request ** RequestMessage method) where - fromJSON (JObject arg) = do - lookup "jsonrpc" arg >>= (guard . (== JString "2.0")) - id <- lookup "id" arg >>= fromJSON - (from ** method) <- lookup "method" arg >>= fromJSON {a = (from ** Method from Request)} - case method of - Shutdown => do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method}) - pure (from ** method ** MkRequestMessage id method (join params)) - WorkspaceSemanticTokensRefresh => - do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method}) - pure (from ** method ** MkRequestMessage id method (join params)) - WorkspaceWorkspaceFolders => - do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method}) - pure (from ** method ** MkRequestMessage id method (join params)) - WorkspaceCodeLensRefresh => - do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method}) - pure (from ** method ** MkRequestMessage id method (join params)) - _ => do params <- lookup "params" arg >>= (fromJSON @{findParamsImpl method}) - pure (from ** method ** MkRequestMessage id method params) - fromJSON _ = neutral - -namespace RequestMessage - export - id : RequestMessage m -> OneOf [Int, String] - id (MkRequestMessage i _ _) = i - - export - method : {0 m : Method from Request} -> RequestMessage m -> Method from Request - method (MkRequestMessage _ m _) = m - - export - params : {0 method : Method from Request} -> RequestMessage method -> MessageParams method - params (MkRequestMessage _ _ p) = p - -||| Maps the message payload to each type of method. -public export -Message : (type : MethodType) -> (Method from type -> Type) -Message Notification = NotificationMessage -Message Request = RequestMessage - -export -FromJSON (from ** type ** method : Method from type ** Message type method) where - fromJSON arg = - (fromJSON arg >>= \(f ** m ** msg) : (from ** method : Method from Request ** RequestMessage method) => pure (f ** _ ** m ** msg)) - <|> (fromJSON arg >>= \(f ** m ** msg) : (from ** method : Method from Notification ** NotificationMessage method) => pure (f ** _ ** m ** msg)) - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage -namespace ErrorCodes - public export - data ErrorCodes - = ParseError - | InvalidRequest - | MethodNotFound - | InvalidParams - | InternalError - | ServerNotInitialized - | UnknownErrorCode - | ContentModified - | RequestCancelled - | JSONRPCReserved Int - | LSPReserved Int - | Custom Int - -export -ToJSON ErrorCodes where - toJSON ParseError = JNumber (-32700) - toJSON InvalidRequest = JNumber (-32600) - toJSON MethodNotFound = JNumber (-32601) - toJSON InvalidParams = JNumber (-32602) - toJSON InternalError = JNumber (-32603) - toJSON ServerNotInitialized = JNumber (-32002) - toJSON UnknownErrorCode = JNumber (-32001) - toJSON ContentModified = JNumber (-32801) - toJSON RequestCancelled = JNumber (-32800) - toJSON (JSONRPCReserved code) = JNumber (cast code) - toJSON (LSPReserved code) = JNumber (cast code) - toJSON (Custom code) = JNumber (cast code) - -export -FromJSON ErrorCodes where - -- TODO: Can't match on negative numbers :(, temporary fix until compiler PR. - fromJSON (JNumber code) = - if code == (-32700) then pure ParseError - else if code == (-32600) then pure InvalidRequest - else if code == (-32601) then pure MethodNotFound - else if code == (-32602) then pure InvalidParams - else if code == (-32603) then pure InternalError - else if code == (-32002) then pure ServerNotInitialized - else if code == (-32001) then pure UnknownErrorCode - else if code == (-32801) then pure ContentModified - else if code == (-32800) then pure RequestCancelled - else if (-32099) <= code && code <= (-32000) then pure (JSONRPCReserved $ cast code) - else if (-32899) <= code && code <= (-32800) then pure (LSPReserved $ cast code) - else pure (Custom $ cast code) - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage -public export -record ResponseError where - constructor MkResponseError - code : ErrorCodes - message : String - data_ : JSON -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{ResponseError} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage -public export -data ResponseMessage : Method from type -> Type where - Success : (id : OneOf [Int, String, Null]) -> (result : ResponseResult method) -> ResponseMessage method - Failure : (id : OneOf [Int, String, Null]) -> (error : ResponseError) -> ResponseMessage method - -export -{method : Method from Request} -> ToJSON (ResponseMessage method) where - toJSON (Success id result) = - JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("result", toJSON @{findResultImpl method} result)]) - toJSON (Failure id error) = - JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("error", toJSON error)]) - -export -FromJSON (ResponseResult method) => FromJSON (ResponseMessage method) where - fromJSON (JObject arg) = do - lookup "jsonrpc" arg >>= (guard . (== JString "2.0")) - id <- lookup "id" arg >>= fromJSON - case lookup "result" arg of - Just v => Success id <$> fromJSON v - Nothing => Failure id <$> (lookup "error" arg >>= fromJSON) - fromJSON _ = neutral - -namespace ResponseMessage - export - id : ResponseMessage method -> OneOf [Int, String, Null] - id (Success i _) = i - id (Failure i _) = i - - export - getResponseId : RequestMessage method -> OneOf [Int, String, Null] - getResponseId = extend . RequestMessage.id diff --git a/src/Language/LSP/Message/Method.idr b/src/Language/LSP/Message/Method.idr deleted file mode 100644 index 8319bfc..0000000 --- a/src/Language/LSP/Message/Method.idr +++ /dev/null @@ -1,337 +0,0 @@ -module Language.LSP.Message.Method - -import public Data.DPair -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -public export -data MethodFrom = Client | Server - -public export -data MethodType = Notification | Request - -public export -data Method : MethodFrom -> MethodType -> Type where - Initialize : Method Client Request - Initialized : Method Client Notification - Shutdown : Method Client Request - Exit : Method Client Notification - SetTrace : Method Client Notification - WindowWorkDoneProgressCancel : Method Client Notification - WorkspaceDidChangeWorkspaceFolders : Method Client Notification - WorkspaceDidChangeConfiguration : Method Client Notification - WorkspaceDidChangeWatchedFiles : Method Client Notification - WorkspaceSymbol : Method Client Request - WorkspaceExecuteCommand : Method Client Request - WorkspaceWillCreateFiles : Method Client Request - TextDocumentDidOpen : Method Client Notification - TextDocumentDidChange : Method Client Notification - TextDocumentWillSave : Method Client Notification - TextDocumentWillSaveWaitUntil : Method Client Request - TextDocumentDidSave : Method Client Notification - TextDocumentDidClose : Method Client Notification - TextDocumentCompletion : Method Client Request - CompletionItemResolve : Method Client Request - TextDocumentHover : Method Client Request - TextDocumentSignatureHelp : Method Client Request - TextDocumentDeclaration : Method Client Request - TextDocumentDefinition : Method Client Request - TextDocumentTypeDefinition : Method Client Request - TextDocumentImplementation : Method Client Request - TextDocumentReferences : Method Client Request - TextDocumentDocumentHighlight : Method Client Request - TextDocumentDocumentSymbol : Method Client Request - TextDocumentCodeAction : Method Client Request - CodeActionResolve : Method Client Request - TextDocumentCodeLens : Method Client Request - CodeLensResolve : Method Client Request - TextDocumentDocumentLink : Method Client Request - DocumentLinkResolve : Method Client Request - TextDocumentDocumentColor : Method Client Request - TextDocumentFormatting : Method Client Request - TextDocumentRangeFormatting : Method Client Request - TextDocumentOnTypeFormatting : Method Client Request - TextDocumentRename : Method Client Request - TextDocumentPrepareRename : Method Client Request - TextDocumentFoldingRange : Method Client Request - TextDocumentSelectionRange : Method Client Request - TextDocumentPrepareCallHierarchy : Method Client Request - CallHierarchyIncomingCalls : Method Client Request - CallHierarchyOutgoingCalls : Method Client Request - TextDocumentSemanticTokensFull : Method Client Request - TextDocumentSemanticTokensFullDelta : Method Client Request - TextDocumentSemanticTokensRange : Method Client Request - TextDocumentLinkedEditingRange : Method Client Request - TextDocumentMoniker : Method Client Request - - LogTrace : Method Server Notification - WindowShowMessage : Method Server Notification - WindowShowMessageRequest : Method Server Request - WindowShowDocument : Method Server Request - WindowLogMessage : Method Server Notification - WindowWorkDoneProgressCreate : Method Server Request - TelemetryEvent : Method Server Notification - ClientRegisterCapability : Method Server Request - ClientUnregisterCapability : Method Server Request - WorkspaceWorkspaceFolders : Method Server Request - WorkspaceConfiguration : Method Server Request - WorkspaceApplyEdit : Method Server Request - TextDocumentPublishDiagnostics : Method Server Notification - WorkspaceCodeLensRefresh : Method Server Request - WorkspaceSemanticTokensRefresh : Method Server Request - - CancelRequest : Method from Notification - Progress : Method from Notification - -export -methodType : Method type from -> MethodType -methodType Initialize = Request -methodType Initialized = Notification -methodType Shutdown = Request -methodType Exit = Notification -methodType SetTrace = Notification -methodType WindowWorkDoneProgressCancel = Notification -methodType WorkspaceDidChangeWorkspaceFolders = Notification -methodType WorkspaceDidChangeConfiguration = Notification -methodType WorkspaceDidChangeWatchedFiles = Notification -methodType WorkspaceSymbol = Request -methodType WorkspaceExecuteCommand = Request -methodType WorkspaceWillCreateFiles = Request -methodType TextDocumentDidOpen = Notification -methodType TextDocumentDidChange = Notification -methodType TextDocumentWillSave = Notification -methodType TextDocumentWillSaveWaitUntil = Request -methodType TextDocumentDidSave = Notification -methodType TextDocumentDidClose = Notification -methodType CompletionItemResolve = Request -methodType TextDocumentHover = Request -methodType TextDocumentSignatureHelp = Request -methodType TextDocumentDeclaration = Request -methodType TextDocumentDefinition = Request -methodType TextDocumentTypeDefinition = Request -methodType TextDocumentImplementation = Request -methodType TextDocumentReferences = Request -methodType TextDocumentDocumentHighlight = Request -methodType TextDocumentDocumentSymbol = Request -methodType TextDocumentCodeAction = Request -methodType CodeActionResolve = Request -methodType TextDocumentCodeLens = Request -methodType CodeLensResolve = Request -methodType TextDocumentDocumentLink = Request -methodType DocumentLinkResolve = Request -methodType TextDocumentDocumentColor = Request -methodType TextDocumentFormatting = Request -methodType TextDocumentRangeFormatting = Request -methodType TextDocumentOnTypeFormatting = Request -methodType TextDocumentRename = Request -methodType TextDocumentPrepareRename = Request -methodType TextDocumentFoldingRange = Request -methodType TextDocumentSelectionRange = Request -methodType TextDocumentPrepareCallHierarchy = Request -methodType CallHierarchyIncomingCalls = Request -methodType CallHierarchyOutgoingCalls = Request -methodType TextDocumentSemanticTokensFull = Request -methodType TextDocumentSemanticTokensFullDelta = Request -methodType TextDocumentSemanticTokensRange = Request -methodType WorkspaceSemanticTokensRefresh = Request -methodType TextDocumentLinkedEditingRange = Request -methodType TextDocumentMoniker = Request -methodType LogTrace = Notification -methodType WindowShowMessage = Notification -methodType WindowShowMessageRequest = Request -methodType WindowShowDocument = Request -methodType WindowLogMessage = Notification -methodType WindowWorkDoneProgressCreate = Request -methodType TelemetryEvent = Notification -methodType ClientRegisterCapability = Request -methodType ClientUnregisterCapability = Request -methodType WorkspaceWorkspaceFolders = Request -methodType WorkspaceConfiguration = Request -methodType WorkspaceApplyEdit = Request -methodType TextDocumentPublishDiagnostics = Notification -methodType TextDocumentCompletion = Request -methodType WorkspaceCodeLensRefresh = Request -methodType CancelRequest = Notification -methodType Progress = Notification - -export -ToJSON (Method type from) where - toJSON Initialize = JString "initialize" - toJSON Initialized = JString "initialized" - toJSON Shutdown = JString "shutdown" - toJSON Exit = JString "exit" - toJSON SetTrace = JString "$/setTrace" - toJSON WindowWorkDoneProgressCancel = JString "window/workDoneProgress/cancel" - toJSON WorkspaceDidChangeWorkspaceFolders = JString "workspace/didChangeWorkspaceFolders" - toJSON WorkspaceDidChangeConfiguration = JString "workspace/didChangeConfiguration" - toJSON WorkspaceDidChangeWatchedFiles = JString "workspace/didChangeWatchedFiles" - toJSON WorkspaceSymbol = JString "workspace/symbol" - toJSON WorkspaceExecuteCommand = JString "workspace/executeCommand" - toJSON WorkspaceWillCreateFiles = JString "workspace/willCreateFiles" - toJSON TextDocumentDidOpen = JString "textDocument/didOpen" - toJSON TextDocumentDidChange = JString "textDocument/didChange" - toJSON TextDocumentWillSave = JString "textDocument/willSave" - toJSON TextDocumentWillSaveWaitUntil = JString "textDocument/willSaveWaitUntil" - toJSON TextDocumentDidSave = JString "textDocument/didSave" - toJSON TextDocumentDidClose = JString "textDocument/didClose" - toJSON CompletionItemResolve = JString "completionItem/resolve" - toJSON TextDocumentHover = JString "textDocument/hover" - toJSON TextDocumentSignatureHelp = JString "textDocument/signatureHelp" - toJSON TextDocumentDeclaration = JString "textDocument/declaration" - toJSON TextDocumentDefinition = JString "textDocument/definition" - toJSON TextDocumentTypeDefinition = JString "textDocument/typeDefinition" - toJSON TextDocumentImplementation = JString "textDocument/implementation" - toJSON TextDocumentReferences = JString "textDocument/references" - toJSON TextDocumentDocumentHighlight = JString "textDocument/documentHighlight" - toJSON TextDocumentDocumentSymbol = JString "textDocument/documentSymbol" - toJSON TextDocumentCodeAction = JString "textDocument/codeAction" - toJSON CodeActionResolve = JString "codeAction/resolve" - toJSON TextDocumentCodeLens = JString "textDocument/codeLens" - toJSON CodeLensResolve = JString "codeLens/resolve" - toJSON TextDocumentDocumentLink = JString "textDocument/documentLink" - toJSON DocumentLinkResolve = JString "documentLink/resolve" - toJSON TextDocumentDocumentColor = JString "textDocument/documentColor" - toJSON TextDocumentFormatting = JString "textDocument/formatting" - toJSON TextDocumentRangeFormatting = JString "textDocument/rangeFormatting" - toJSON TextDocumentOnTypeFormatting = JString "textDocument/onTypeFormatting" - toJSON TextDocumentRename = JString "textDocument/rename" - toJSON TextDocumentPrepareRename = JString "textDocument/prepareRename" - toJSON TextDocumentFoldingRange = JString "textDocument/foldingRange" - toJSON TextDocumentSelectionRange = JString "textDocument/selectionRange" - toJSON TextDocumentPrepareCallHierarchy = JString "textDocument/prepareCallHierarchy" - toJSON CallHierarchyIncomingCalls = JString "callHierarchy/incomingCalls" - toJSON CallHierarchyOutgoingCalls = JString "callHierarchy/outgoingCalls" - toJSON TextDocumentSemanticTokensFull = JString "textDocument/semanticTokens/full" - toJSON TextDocumentSemanticTokensFullDelta = JString "textDocument/semanticTokens/full/delta" - toJSON TextDocumentSemanticTokensRange = JString "textDocument/semanticTokens/range" - toJSON WorkspaceSemanticTokensRefresh = JString "workspace/semanticTokens/refresh" - toJSON TextDocumentLinkedEditingRange = JString "textDocument/linkedEditingRange" - toJSON TextDocumentMoniker = JString "textDocument/moniker" - toJSON LogTrace = JString "$/logTrace" - toJSON WindowShowMessage = JString "window/showMessage" - toJSON WindowShowMessageRequest = JString "window/showMessageRequest" - toJSON WindowShowDocument = JString "window/showDocument" - toJSON WindowLogMessage = JString "window/logMessage" - toJSON WindowWorkDoneProgressCreate = JString "window/workDoneProgress/create" - toJSON TelemetryEvent = JString "telemetry/event" - toJSON ClientRegisterCapability = JString "client/registerCapability" - toJSON ClientUnregisterCapability = JString "client/unregisterCapability" - toJSON WorkspaceWorkspaceFolders = JString "workspace/workspaceFolders" - toJSON WorkspaceConfiguration = JString "workspace/configuration" - toJSON WorkspaceApplyEdit = JString "workspace/applyEdit" - toJSON TextDocumentPublishDiagnostics = JString "textDocument/publishDiagnostics" - toJSON TextDocumentCompletion = JString "textDocument/completion" - toJSON WorkspaceCodeLensRefresh = JString "workspace/codeLens/refresh" - toJSON CancelRequest = JString "$/cancelRequest" - toJSON Progress = JString "$/progress" - -export -FromJSON (Method Client Notification) where - fromJSON (JString "initialized") = pure Initialized - fromJSON (JString "exit") = pure Exit - fromJSON (JString "$/setTrace") = pure SetTrace - fromJSON (JString "window/workDoneProgress/cancel") = pure WindowWorkDoneProgressCancel - fromJSON (JString "workspace/didChangeWorkspaceFolders") = pure WorkspaceDidChangeWorkspaceFolders - fromJSON (JString "workspace/didChangeConfiguration") = pure WorkspaceDidChangeConfiguration - fromJSON (JString "workspace/didChangeWatchedFiles") = pure WorkspaceDidChangeWatchedFiles - fromJSON (JString "textDocument/didOpen") = pure TextDocumentDidOpen - fromJSON (JString "textDocument/didChange") = pure TextDocumentDidChange - fromJSON (JString "textDocument/willSave") = pure TextDocumentWillSave - fromJSON (JString "textDocument/didSave") = pure TextDocumentDidSave - fromJSON (JString "textDocument/didClose") = pure TextDocumentDidClose - fromJSON (JString "$/cancelRequest") = pure CancelRequest - fromJSON (JString "$/progress") = pure Progress - fromJSON _ = neutral - -export -FromJSON (Method Client Request) where - fromJSON (JString "initialize") = pure Initialize - fromJSON (JString "shutdown") = pure Shutdown - fromJSON (JString "workspace/symbol") = pure WorkspaceSymbol - fromJSON (JString "workspace/executeCommand") = pure WorkspaceExecuteCommand - fromJSON (JString "workspace/willCreateFiles") = pure WorkspaceWillCreateFiles - fromJSON (JString "textDocument/willSaveWaitUntil") = pure TextDocumentWillSaveWaitUntil - fromJSON (JString "textDocument/completion") = pure TextDocumentCompletion - fromJSON (JString "completionItem/resolve") = pure CompletionItemResolve - fromJSON (JString "textDocument/hover") = pure TextDocumentHover - fromJSON (JString "textDocument/signatureHelp") = pure TextDocumentSignatureHelp - fromJSON (JString "textDocument/declaration") = pure TextDocumentDeclaration - fromJSON (JString "textDocument/definition") = pure TextDocumentDefinition - fromJSON (JString "textDocument/typeDefinition") = pure TextDocumentTypeDefinition - fromJSON (JString "textDocument/implementation") = pure TextDocumentImplementation - fromJSON (JString "textDocument/references") = pure TextDocumentReferences - fromJSON (JString "textDocument/documentHighlight") = pure TextDocumentDocumentHighlight - fromJSON (JString "textDocument/documentSymbol") = pure TextDocumentDocumentSymbol - fromJSON (JString "textDocument/codeAction") = pure TextDocumentCodeAction - fromJSON (JString "codeAction/resolve") = pure CodeActionResolve - fromJSON (JString "textDocument/codeLens") = pure TextDocumentCodeLens - fromJSON (JString "codeLens/resolve") = pure CodeLensResolve - fromJSON (JString "textDocument/documentLink") = pure TextDocumentDocumentLink - fromJSON (JString "documentLink/resolve") = pure DocumentLinkResolve - fromJSON (JString "textDocument/documentColor") = pure TextDocumentDocumentColor - fromJSON (JString "textDocument/formatting") = pure TextDocumentFormatting - fromJSON (JString "textDocument/rangeFormatting") = pure TextDocumentRangeFormatting - fromJSON (JString "textDocument/onTypeFormatting") = pure TextDocumentOnTypeFormatting - fromJSON (JString "textDocument/rename") = pure TextDocumentRename - fromJSON (JString "textDocument/prepareRename") = pure TextDocumentPrepareRename - fromJSON (JString "textDocument/foldingRange") = pure TextDocumentFoldingRange - fromJSON (JString "textDocument/selectionRange") = pure TextDocumentSelectionRange - fromJSON (JString "textDocument/prepareCallHierarchy") = pure TextDocumentPrepareCallHierarchy - fromJSON (JString "callHierarchy/incomingCalls") = pure CallHierarchyIncomingCalls - fromJSON (JString "callHierarchy/outgoingCalls") = pure CallHierarchyOutgoingCalls - fromJSON (JString "textDocument/semanticTokens/full") = pure TextDocumentSemanticTokensFull - fromJSON (JString "textDocument/semanticTokens/full/delta") = pure TextDocumentSemanticTokensFullDelta - fromJSON (JString "textDocument/semanticTokens/range") = pure TextDocumentSemanticTokensRange - fromJSON (JString "textDocument/linkedEditingRange") = pure TextDocumentLinkedEditingRange - fromJSON (JString "textDocument/moniker") = pure TextDocumentMoniker - fromJSON _ = neutral - -export -FromJSON (Method Server Notification) where - fromJSON (JString "$/logTrace") = pure LogTrace - fromJSON (JString "window/showMessage") = pure WindowShowMessage - fromJSON (JString "window/logMessage") = pure WindowLogMessage - fromJSON (JString "telemetry/event") = pure TelemetryEvent - fromJSON (JString "textDocument/publishDiagnostics") = pure TextDocumentPublishDiagnostics - fromJSON (JString "$/cancelRequest") = pure CancelRequest - fromJSON (JString "$/progress") = pure Progress - fromJSON _ = neutral - -export -FromJSON (Method Server Request) where - fromJSON (JString "window/showMessageRequest") = pure WindowShowMessageRequest - fromJSON (JString "window/showDocument") = pure WindowShowDocument - fromJSON (JString "window/workDoneProgress/create") = pure WindowWorkDoneProgressCreate - fromJSON (JString "client/registerCapability") = pure ClientRegisterCapability - fromJSON (JString "client/unregisterCapability") = pure ClientUnregisterCapability - fromJSON (JString "workspace/workspaceFolders") = pure WorkspaceWorkspaceFolders - fromJSON (JString "workspace/configuration") = pure WorkspaceConfiguration - fromJSON (JString "workspace/applyEdit") = pure WorkspaceApplyEdit - fromJSON (JString "workspace/codeLens/refresh") = pure WorkspaceCodeLensRefresh - fromJSON (JString "workspace/semanticTokens/refresh") = pure WorkspaceSemanticTokensRefresh - fromJSON _ = neutral - -export -FromJSON (from ** Method from Notification) where - fromJSON arg = - (fromJSON arg >>= \meth : Method Client Notification => pure (_ ** meth)) - <|> (fromJSON arg >>= \meth : Method Server Notification => pure (_ ** meth)) - -export -FromJSON (from ** Method from Request) where - fromJSON arg = - (fromJSON arg >>= \meth : Method Client Request => pure (_ ** meth)) - <|> (fromJSON arg >>= \meth : Method Server Request => pure (_ ** meth)) - -export -FromJSON (from ** type ** Method from type) where - fromJSON arg = - (fromJSON arg >>= \meth : Method Client Notification => pure (_ ** _ ** meth)) - <|> (fromJSON arg >>= \meth : Method Client Request => pure (_ ** _ ** meth)) - <|> (fromJSON arg >>= \meth : Method Server Notification => pure (_ ** _ ** meth)) - <|> (fromJSON arg >>= \meth : Method Server Request => pure (_ ** _ ** meth)) diff --git a/src/Language/LSP/Message/Moniker.idr b/src/Language/LSP/Message/Moniker.idr deleted file mode 100644 index 83042b2..0000000 --- a/src/Language/LSP/Message/Moniker.idr +++ /dev/null @@ -1,94 +0,0 @@ -module Language.LSP.Message.Moniker - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker -public export -record MonikerClientCapabilities where - constructor MkMonikerClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{MonikerClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker -public export -record MonikerOptions where - constructor MkMonikersOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{MonikerOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker -public export -record MonikerRegistrationOptions where - constructor MkMonikersRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{MonikerRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker -public export -record MonikerParams where - constructor MkMonikersParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{MonikerParams} - -namespace UniquenessLevel - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker - public export - data UniquenessLevel = Document | Project | Group | Scheme | Global - -export -ToJSON UniquenessLevel where - toJSON Document = JString "document" - toJSON Project = JString "project" - toJSON Group = JString "group" - toJSON Scheme = JString "scheme" - toJSON Global = JString "global" - -export -FromJSON UniquenessLevel where - fromJSON (JString "document") = pure Document - fromJSON (JString "project") = pure Project - fromJSON (JString "group") = pure Group - fromJSON (JString "scheme") = pure Scheme - fromJSON (JString "global") = pure Global - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker -namespace MonikerKind - public export - data MonikerKind = Import | Export | Local - -export -ToJSON MonikerKind where - toJSON Import = JString "import" - toJSON Export = JString "export" - toJSON Local = JString "local" - -export -FromJSON MonikerKind where - fromJSON (JString "import") = pure Import - fromJSON (JString "export") = pure Export - fromJSON (JString "local") = pure Local - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker -public export -record Moniker where - constructor MkMoniker - scheme : String - identifier : String - unique : UniquenessLevel - kind : Maybe MonikerKind -%runElab deriveJSON defaultOpts `{Moniker} diff --git a/src/Language/LSP/Message/Progress.idr b/src/Language/LSP/Message/Progress.idr deleted file mode 100644 index ddb9d6c..0000000 --- a/src/Language/LSP/Message/Progress.idr +++ /dev/null @@ -1,61 +0,0 @@ -module Language.LSP.Message.Progress - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#progress -public export -ProgressToken : Type -ProgressToken = OneOf [Int, String] - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#clientInitiatedProgress -public export -record WorkDoneProgressOptions where - constructor MkWorkDoneProgressOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{WorkDoneProgressOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#clientInitiatedProgress -public export -record WorkDoneProgressParams where - constructor MkWorkDoneProgressParams - workDoneToken : Maybe ProgressToken -%runElab deriveJSON defaultOpts `{WorkDoneProgressParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#partialResultParams -public export -record PartialResultParams where - constructor MkPartialResultParams - partialResultToken : Maybe ProgressToken -%runElab deriveJSON defaultOpts `{PartialResultParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressBegin -public export -record WorkDoneProgressBegin where - constructor MkWorkDoneProgressBegin - title : String - cancellable : Maybe Bool - message : Maybe String - percentage : Maybe Int -%runElab deriveJSON ({staticFields := [("kind", JString "begin")]} defaultOpts) `{WorkDoneProgressBegin} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressReport -public export -record WorkDoneProgressReport where - constructor MkWorkDoneProgressReport - cancellable : Maybe Bool - message : Maybe String - percentage : Maybe Int -%runElab deriveJSON ({staticFields := [("kind", JString "report")]} defaultOpts) `{WorkDoneProgressReport} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressEnd -public export -record WorkDoneProgressEnd where - constructor MkWorkDoneProgressEnd - message : Maybe String -%runElab deriveJSON ({staticFields := [("kind", JString "end")]} defaultOpts) `{WorkDoneProgressEnd} diff --git a/src/Language/LSP/Message/References.idr b/src/Language/LSP/Message/References.idr deleted file mode 100644 index cd274b3..0000000 --- a/src/Language/LSP/Message/References.idr +++ /dev/null @@ -1,52 +0,0 @@ -module Language.LSP.Message.References - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references -public export -record ReferenceClientCapabilities where - constructor MkReferenceClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{ReferenceClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references -public export -record ReferenceOptions where - constructor MkReferenceOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{ReferenceOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references -public export -record ReferenceRegistrationOptions where - constructor MkReferenceRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{ReferenceRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references -public export -record ReferenceContext where - constructor MkReferenceContext - includeDeclaration : Bool -%runElab deriveJSON defaultOpts `{ReferenceContext} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references -public export -record ReferenceParams where - constructor MkReferenceParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position - context : ReferenceContext -%runElab deriveJSON defaultOpts `{ReferenceParams} diff --git a/src/Language/LSP/Message/Registration.idr b/src/Language/LSP/Message/Registration.idr deleted file mode 100644 index 638a845..0000000 --- a/src/Language/LSP/Message/Registration.idr +++ /dev/null @@ -1,41 +0,0 @@ -module Language.LSP.Message.Registration - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_registerCapability -public export -record Registration where - constructor MkRegistration - id : String - method : String - registerOptions : Maybe JSON -%runElab deriveJSON defaultOpts `{Registration} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_registerCapability -public export -record RegistrationParams where - constructor MkRegistrationParams - registrations : List Registration -%runElab deriveJSON defaultOpts `{RegistrationParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_unregisterCapability -public export -record Unregistration where - constructor MkUnregistration - id : String - method : String -%runElab deriveJSON defaultOpts `{Unregistration} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_unregisterCapability -public export -record UnregistrationParams where - constructor MkUnregistrationParams - -- NOTE: not my typo, but see the specification link in the record documentation - unregisterations : List Unregistration -%runElab deriveJSON defaultOpts `{UnregistrationParams} diff --git a/src/Language/LSP/Message/RegularExpressions.idr b/src/Language/LSP/Message/RegularExpressions.idr deleted file mode 100644 index c62febd..0000000 --- a/src/Language/LSP/Message/RegularExpressions.idr +++ /dev/null @@ -1,17 +0,0 @@ -module Language.LSP.Message.RegularExpressions - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#regExp -public export -record RegularExpressionsClientCapabilities where - constructor MkRegularExpressionsClientCapabilities - engine : String - version : Maybe String -%runElab deriveJSON defaultOpts `{RegularExpressionsClientCapabilities} diff --git a/src/Language/LSP/Message/Rename.idr b/src/Language/LSP/Message/Rename.idr deleted file mode 100644 index 3be8222..0000000 --- a/src/Language/LSP/Message/Rename.idr +++ /dev/null @@ -1,86 +0,0 @@ -module Language.LSP.Message.Rename - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -namespace PrepareSupportDefaultBehaviour - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename - public export - data PrepareSupportDefaultBehaviour = Identifier - -export -ToJSON PrepareSupportDefaultBehaviour where - toJSON Identifier = JNumber 1 - -export -FromJSON PrepareSupportDefaultBehaviour where - fromJSON (JNumber 1) = pure Identifier - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename -public export -record RenameClientCapabilities where - constructor MkRenameClientCapabilities - dynamicRegistration : Maybe Bool - prepareSupport : Maybe Bool - prepareSupportDefaultBehaviour : Maybe PrepareSupportDefaultBehaviour - honorsChangeAnnotation : Maybe Bool -%runElab deriveJSON defaultOpts `{RenameClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename -public export -record RenameOptions where - constructor MkRenameOptions - workDoneProgress : Maybe Bool - prepareProvider : Maybe Bool -%runElab deriveJSON defaultOpts `{RenameOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename -public export -record RenameRegistrationOptions where - constructor MkRenameRegistrationOptions - workDoneProgress : Maybe Bool - prepareProvider : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{RenameRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename -public export -record RenameParams where - constructor MkRenameParams - workDoneToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - newName : String -%runElab deriveJSON defaultOpts `{RenameParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename -public export -record PrepareRenameParams where - constructor MkPrepareRenameParams - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{PrepareRenameParams} - -namespace PrepareRenameResponse - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename - public export - record PrepareRenameDefaultResponse where - constructor MkPrepareRenameDefaultResponse - defaultBehaviour : Bool - %runElab deriveJSON defaultOpts `{PrepareRenameDefaultResponse} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename - public export - record PrepareRenamePlaceholderResponse where - constructor MkPrepareRenamePlaceholderResponse - range : Range - placeholder : String - %runElab deriveJSON defaultOpts `{PrepareRenamePlaceholderResponse} diff --git a/src/Language/LSP/Message/SelectionRange.idr b/src/Language/LSP/Message/SelectionRange.idr deleted file mode 100644 index 68b23ef..0000000 --- a/src/Language/LSP/Message/SelectionRange.idr +++ /dev/null @@ -1,66 +0,0 @@ -module Language.LSP.Message.SelectionRange - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange -public export -record SelectionRangeClientCapabilities where - constructor MkSelectionRangeClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{SelectionRangeClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange -public export -record SelectionRangeOptions where - constructor MkSelectionRangeOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{SelectionRangeOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange -public export -record SelectionRangeRegistrationOptions where - constructor MkSelectionRangeRegistrationOptions - workDoneProgress : Maybe Bool - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe String -%runElab deriveJSON defaultOpts `{SelectionRangeRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange -public export -record SelectionRangeParams where - constructor MkSelectionRangeParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - positions : List Position -%runElab deriveJSON defaultOpts `{SelectionRangeParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange -public export -record SelectionRange where - constructor MkSelectionRange - range : Range - parent : Maybe (Inf SelectionRange) - -export -- FIXME: Can I avoid asser_total? Maybe indexing by the depth of the structure? -ToJSON SelectionRange where - toJSON (MkSelectionRange range parent) = assert_total $ - JObject (catMaybes [ Just ("range", toJSON range) - , (MkPair "parent" . toJSON) <$> parent - ]) - -export covering -FromJSON SelectionRange where - fromJSON (JObject arg) = - pure MkSelectionRange <*> (lookup "range" arg >>= fromJSON) - <*> (pure $ lookup "parent" arg >>= fromJSON) - fromJSON _ = neutral diff --git a/src/Language/LSP/Message/SemanticTokens.idr b/src/Language/LSP/Message/SemanticTokens.idr deleted file mode 100644 index efea0c8..0000000 --- a/src/Language/LSP/Message/SemanticTokens.idr +++ /dev/null @@ -1,158 +0,0 @@ -module Language.LSP.Message.SemanticTokens - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -namespace SemanticTokenClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens - public export - record SemanticTokenRequestsFull where - constructor MkSemanticTokenRequestsFull - delta : Maybe Bool - %runElab deriveJSON defaultOpts `{SemanticTokenRequestsFull} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens - public export - record SemanticTokenRequests where - constructor MkSemanticTokenRequests - range : Maybe (OneOf [Bool, ()]) - full : Maybe (OneOf [Bool, SemanticTokenRequestsFull]) - %runElab deriveJSON defaultOpts `{SemanticTokenRequests} - -namespace TokenFormat - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens - public export - data TokenFormat = Relative - -export -ToJSON TokenFormat where - toJSON Relative = JString "relative" - -export -FromJSON TokenFormat where - fromJSON (JString "relative") = pure Relative - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensLegend where - constructor MkSemanticTokensLegend - tokenTypes : List String - tokenModifiers : List String -%runElab deriveJSON defaultOpts `{SemanticTokensLegend} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensClientCapabilities where - constructor MkSemanticTokensClientCapabilities - dynamicRegistration : Maybe Bool - requests : SemanticTokenRequests - tokenTypes : List String - tokenModifiers : List String - formats : List TokenFormat - overlappingTokenSupport : Maybe Bool - multilineTokenSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{SemanticTokensClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensOptions where - constructor MkSemanticTokensOptions - legend : SemanticTokensLegend - range : Maybe (OneOf [Bool, ()]) - full : Maybe (OneOf [Bool, SemanticTokenRequestsFull]) -%runElab deriveJSON defaultOpts `{SemanticTokensOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensRegistrationOptions where - constructor MkSemanticTokensRegistrationOptions - legend : SemanticTokensLegend - range : Maybe (OneOf [Bool, ()]) - full : Maybe (OneOf [Bool, SemanticTokenRequestsFull]) - documentSelector : OneOf [DocumentSelector, Null] - id : Maybe Bool -%runElab deriveJSON defaultOpts `{SemanticTokensRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensParams where - constructor MkSemanticTokensParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{SemanticTokensParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokens where - constructor MkSemanticTokens - resultId : Maybe String - data_ : List Int -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{SemanticTokens} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensPartialResult where - constructor MkSemanticTokensPartialResult - data_ : List Int -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{SemanticTokensPartialResult} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensDeltaParams where - constructor MkSemanticTokensDeltaParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - previousResultId : String -%runElab deriveJSON defaultOpts `{SemanticTokensDeltaParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensEdit where - constructor MkSemanticTokensEdit - start : Int - deleteCount : Int - data_ : Maybe (List Int) -%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{SemanticTokensEdit} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensDelta where - constructor MkSemanticTokensDelta - resultId : Maybe String - edits : List SemanticTokensEdit -%runElab deriveJSON defaultOpts `{SemanticTokensDelta} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensDeltaPartialResult where - constructor MkSemanticTokensDeltaPartialResult - edits : List SemanticTokensEdit -%runElab deriveJSON defaultOpts `{SemanticTokensDeltaPartialResult} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensRangeParams where - constructor MkSemanticTokensRangeParams - workDoneToken : Maybe ProgressToken - partialResultToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - range : Range -%runElab deriveJSON defaultOpts `{SemanticTokensRangeParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_semanticTokens -public export -record SemanticTokensWorkspaceClientCapabilities where - constructor MkSemanticTokensWorkspaceClientCapabilities - refreshSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{SemanticTokensWorkspaceClientCapabilities} diff --git a/src/Language/LSP/Message/ServerCapabilities.idr b/src/Language/LSP/Message/ServerCapabilities.idr deleted file mode 100644 index 5ce0e17..0000000 --- a/src/Language/LSP/Message/ServerCapabilities.idr +++ /dev/null @@ -1,107 +0,0 @@ -module Language.LSP.Message.ServerCapabilities - -import Data.SortedMap -import Language.JSON -import Language.LSP.Message.CallHierarchy -import Language.LSP.Message.Cancel -import Language.LSP.Message.CodeAction -import Language.LSP.Message.CodeLens -import Language.LSP.Message.Command -import Language.LSP.Message.Completion -import Language.LSP.Message.Declaration -import Language.LSP.Message.Definition -import Language.LSP.Message.Derive -import Language.LSP.Message.Diagnostics -import Language.LSP.Message.DocumentColor -import Language.LSP.Message.DocumentFormatting -import Language.LSP.Message.DocumentHighlight -import Language.LSP.Message.DocumentLink -import Language.LSP.Message.DocumentSymbols -import Language.LSP.Message.FoldingRange -import Language.LSP.Message.Hover -import Language.LSP.Message.Implementation -import Language.LSP.Message.LinkedEditingRange -import Language.LSP.Message.Location -import Language.LSP.Message.Markup -import Language.LSP.Message.Method -import Language.LSP.Message.Moniker -import Language.LSP.Message.Progress -import Language.LSP.Message.References -import Language.LSP.Message.Registration -import Language.LSP.Message.RegularExpressions -import Language.LSP.Message.Rename -import Language.LSP.Message.SelectionRange -import Language.LSP.Message.SemanticTokens -import Language.LSP.Message.SignatureHelp -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Trace -import Language.LSP.Message.Utils -import Language.LSP.Message.Window -import Language.LSP.Message.Workspace -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record FileOperationsServerCapabilities where - constructor MkFileOperationsServerCapabilities - didCreate : Maybe FileOperationRegistrationOptions - willCreate : Maybe FileOperationRegistrationOptions - didRename : Maybe FileOperationRegistrationOptions - willRename : Maybe FileOperationRegistrationOptions - didDelete : Maybe FileOperationRegistrationOptions - willDelete : Maybe FileOperationRegistrationOptions -%runElab deriveJSON defaultOpts `{FileOperationsServerCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record WorkspaceServerCapabilities where - constructor MkWorkspaceServerCapabilities - workspaceFolders : Maybe WorkspaceFoldersServerCapabilities - fileOperations : Maybe FileOperationsServerCapabilities -%runElab deriveJSON defaultOpts `{WorkspaceServerCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record ServerCapabilities where - constructor MkServerCapabilities - textDocumentSync : Maybe (OneOf [TextDocumentSyncOptions, TextDocumentSyncKind]) - completionProvider : Maybe CompletionOptions - hoverProvider : Maybe (OneOf [Bool, HoverOptions]) - signatureHelpProvider : Maybe SignatureHelpOptions - declarationProvider : Maybe (OneOf [Bool, DeclarationOptions, DeclarationRegistrationOptions]) - definitionProvider : Maybe (OneOf [Bool, DefinitionOptions, DefinitionRegistrationOptions]) - typeDefinitionProvider : Maybe (OneOf [Bool, TypeDefinitionOptions, TypeDefinitionRegistrationOptions]) - implementationProvider : Maybe (OneOf [Bool, ImplementationOptions, ImplementationRegistrationOptions]) - referencesProvider : Maybe (OneOf [Bool, ReferenceOptions]) - documentHighlightProvider : Maybe (OneOf [Bool, DocumentHighlightOptions]) - documentSymbolProvider : Maybe (OneOf [Bool, DocumentSymbolOptions]) - codeActionProvider : Maybe (OneOf [Bool, CodeActionOptions]) - codeLensProvider : Maybe CodeLensOptions - documentLinkProvider : Maybe DocumentLinkOptions - colorProvider : Maybe (OneOf [Bool, DocumentColorOptions, DocumentColorRegistrationOptions]) - documentFormattingProvider : Maybe (OneOf [Bool, DocumentFormattingOptions]) - documentRangeFormattingProvider : Maybe (OneOf [Bool, DocumentRangeFormattingOptions]) - documentOnTypeFormattingProvider : Maybe DocumentOnTypeFormattingOptions - renameProvider : Maybe (OneOf [Bool, RenameOptions]) - foldingRangeProvider : Maybe (OneOf [Bool, FoldingRangeOptions, FoldingRangeRegistrationOptions]) - executeCommandProvider : Maybe ExecuteCommandOptions - selectionRangeProvider : Maybe (OneOf [Bool, SelectionRangeOptions, SelectionRangeRegistrationOptions]) - linkedEditingRangeProvider : Maybe (OneOf [Bool, LinkedEditingRangeOptions, LinkedEditingRangeRegistrationOptions]) - callHierarchyProvider : Maybe (OneOf [Bool, CallHierarchyOptions, CallHierarchyRegistrationOptions]) - semanticTokensProvider : Maybe (OneOf [SemanticTokensOptions, SemanticTokensRegistrationOptions]) - monikerProvider : Maybe (OneOf [Bool, MonikerOptions, MonikerRegistrationOptions]) - workspaceSymbolProvider : Maybe (OneOf [Bool, WorkspaceSymbolOptions]) - workspace : Maybe WorkspaceServerCapabilities - experimental : Maybe JSON -%runElab deriveJSON defaultOpts `{ServerCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize -public export -record ServerInfo where - constructor MkServerInfo - name : String - version : Maybe String -%runElab deriveJSON defaultOpts `{ServerInfo} diff --git a/src/Language/LSP/Message/SignatureHelp.idr b/src/Language/LSP/Message/SignatureHelp.idr deleted file mode 100644 index ac11fd0..0000000 --- a/src/Language/LSP/Message/SignatureHelp.idr +++ /dev/null @@ -1,124 +0,0 @@ -module Language.LSP.Message.SignatureHelp - -import Language.JSON -import Language.LSP.Message.Location -import Language.LSP.Message.Derive -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.LSP.Message.Markup -import Language.LSP.Message.TextDocument -import Language.LSP.Message.Progress -import Language.Reflection - -%language ElabReflection -%default total - -namespace SignatureHelpClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp - public export - record SignatureHelpParameterInformation where - constructor MkSignatureHelpParameterInformation - labelOffsetSupport : Maybe Bool - %runElab deriveJSON defaultOpts `{SignatureHelpParameterInformation} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp - public export - record SignatureHelpInformation where - constructor MkSignatureHelpInformation - documentationFormat : Maybe (List MarkupKind) - parameterInformation : Maybe SignatureHelpParameterInformation - activeParameterSupport : Maybe Bool - %runElab deriveJSON defaultOpts `{SignatureHelpInformation} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record SignatureHelpClientCapabilities where - constructor MkSignatureHelpClientCapabilities - dynamicRegistration : Maybe Bool - signatureInformation : Maybe SignatureHelpInformation - contextSupport : Maybe Bool -%runElab deriveJSON defaultOpts `{SignatureHelpClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record SignatureHelpOptions where - constructor MkSignatureHelpOptions - workDoneProgress : Maybe Bool - triggerCharacters : Maybe (List Char) - retriggerCharacters : Maybe (List Char) -%runElab deriveJSON defaultOpts `{SignatureHelpOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record SignatureHelpRegistrationOptions where - constructor MkSignatureHelpRegistrationOptions - workDoneProgress : Maybe Bool - triggerCharacters : Maybe (List Char) - retriggerCharacters : Maybe (List Char) - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{SignatureHelpRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -namespace SignatureHelpTriggerKind - public export - data SignatureHelpTriggerKind = Invoked | TriggerCharacter | ContentChange - -export -ToJSON SignatureHelpTriggerKind where - toJSON Invoked = JNumber 1 - toJSON TriggerCharacter = JNumber 2 - toJSON ContentChange = JNumber 3 - -export -FromJSON SignatureHelpTriggerKind where - fromJSON (JNumber 1) = pure Invoked - fromJSON (JNumber 2) = pure TriggerCharacter - fromJSON (JNumber 3) = pure ContentChange - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record ParameterInformation where - constructor MkParameterInformation - label : OneOf [String, (Int, Int)] - documentation : Maybe (OneOf [String, MarkupContent]) -%runElab deriveJSON defaultOpts `{ParameterInformation} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record SignatureInformation where - constructor MkSignatureInformation - label : String - documentation : Maybe (OneOf [String, MarkupContent]) - parameters_ : Maybe (List ParameterInformation) - activeParameter : Maybe Int -%runElab deriveJSON ({renames := [("parameters_", "parameters")]} defaultOpts) `{SignatureInformation} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record SignatureHelp where - constructor MkSignatureHelp - signatures : List SignatureInformation - activeSignature : Maybe Int - activeParameter : Maybe Int -%runElab deriveJSON defaultOpts `{SignatureHelp} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record SignatureHelpContext where - constructor MkSignatureHelpContext - triggerKind : SignatureHelpTriggerKind - triggerCharacter : Maybe Char - isRetrigger : Bool - activeSignatureHelp : Maybe SignatureHelp -%runElab deriveJSON defaultOpts `{SignatureHelpContext} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp -public export -record SignatureHelpParams where - constructor MkSignatureHelpParams - workDoneToken : Maybe ProgressToken - textDocument : TextDocumentIdentifier - position : Position - context : Maybe SignatureHelpContext -%runElab deriveJSON defaultOpts `{SignatureHelpParams} diff --git a/src/Language/LSP/Message/TextDocument.idr b/src/Language/LSP/Message/TextDocument.idr deleted file mode 100644 index c371618..0000000 --- a/src/Language/LSP/Message/TextDocument.idr +++ /dev/null @@ -1,206 +0,0 @@ -module Language.LSP.Message.TextDocument - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentIdentifier -public export -record TextDocumentIdentifier where - constructor MkTextDocumentIdentifier - uri : DocumentURI -%runElab deriveJSON defaultOpts `{TextDocumentIdentifier} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier -public export -record VersionedTextDocumentIdentifier where - constructor MkVersionedTextDocumentIdentifier - uri : DocumentURI - version : Int -%runElab deriveJSON defaultOpts `{VersionedTextDocumentIdentifier} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier -public export -record OptionalVersionedTextDocumentIdentifier where - constructor MkOptionalVersionedTextDocumentIdentifier - uri : DocumentURI - version : Maybe Int -%runElab deriveJSON defaultOpts `{OptionalVersionedTextDocumentIdentifier} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentItem -public export -record TextDocumentItem where - constructor MkTextDocumentItem - uri : DocumentURI - languageId : String - version : Int - text : String -%runElab deriveJSON defaultOpts `{TextDocumentItem} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentPositionParams -public export -record TextDocumentPositionParams where - constructor MkTextDocumentPositionParams - textDocument : TextDocumentIdentifier - position : Position -%runElab deriveJSON defaultOpts `{TextDocumentPositionParams} - -namespace TextDocumentSyncKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_synchronization - public export - data TextDocumentSyncKind = None | Full | Incremental - -export -ToJSON TextDocumentSyncKind where - toJSON None = JNumber 0 - toJSON Full = JNumber 1 - toJSON Incremental = JNumber 2 - -export -FromJSON TextDocumentSyncKind where - fromJSON (JNumber 0) = pure None - fromJSON (JNumber 1) = pure Full - fromJSON (JNumber 2) = pure Incremental - fromJSON _ = Nothing - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didOpen -public export -record DidOpenTextDocumentParams where - constructor MkDidOpenTextDocumentParams - textDocument : TextDocumentItem -%runElab deriveJSON defaultOpts `{DidOpenTextDocumentParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter -public export -record DocumentFilter where - constructor MkDocumentFilter - language : Maybe String - scheme : Maybe String - pattern : Maybe String -%runElab deriveJSON defaultOpts `{DocumentFilter} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter -public export -DocumentSelector : Type -DocumentSelector = List DocumentFilter - -public export -record TextDocumentRegistrationOptions where - constructor MkTextDocumentRegistrationOptions - documentSelector : OneOf [DocumentSelector, Null] -%runElab deriveJSON defaultOpts `{TextDocumentRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentRegistrationOptions -public export -record TextDocumentChangeRegistrationOptions where - constructor MkTextDocumentChangeRegistrationOptions - syncKind : TextDocumentSyncKind -%runElab deriveJSON defaultOpts `{TextDocumentChangeRegistrationOptions} - -namespace DidChangeTextDocumentParams - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange - public export - record TextDocumentContentChangeEvent where - constructor MkTextDocumentContentChangeEvent - text : String - %runElab deriveJSON defaultOpts `{TextDocumentContentChangeEvent} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange - public export - record TextDocumentContentChangeEventWithRange where - constructor MkTextDocumentContentChangeEventWithRange - range : Range - rangeLength : Maybe Int - text : String - %runElab deriveJSON defaultOpts `{TextDocumentContentChangeEventWithRange} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange -public export -record DidChangeTextDocumentParams where - constructor MkDidChangeTextDocumentParams - textDocument : VersionedTextDocumentIdentifier - contentChanges : List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange]) -%runElab deriveJSON defaultOpts `{DidChangeTextDocumentParams} - -namespace TextDocumentSaveReason - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave - public export - data TextDocumentSaveReason = Manual | AfterDelay | FocusOut - -export -ToJSON TextDocumentSaveReason where - toJSON Manual = JNumber 1 - toJSON AfterDelay = JNumber 2 - toJSON FocusOut = JNumber 3 - -export -FromJSON TextDocumentSaveReason where - fromJSON (JNumber 1) = pure Manual - fromJSON (JNumber 2) = pure AfterDelay - fromJSON (JNumber 3) = pure FocusOut - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave -public export -record WillSaveTextDocumentParams where - constructor MkWillSaveTextDocumentParams - textDocument : TextDocumentIdentifier - reason : TextDocumentSaveReason -%runElab deriveJSON defaultOpts `{WillSaveTextDocumentParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave -public export -record SaveOptions where - constructor MkSaveOptions - includeText : Maybe Bool -%runElab deriveJSON defaultOpts `{SaveOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave -public export -record TextDocumentSaveRegistrationOptions where - constructor MkTextDocumentSaveRegistrationOptions - documentSelector : OneOf [DocumentSelector, Null] - includeText : Maybe Bool -%runElab deriveJSON defaultOpts `{TextDocumentSaveRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave -public export -record DidSaveTextDocumentParams where - constructor MkDidSaveTextDocumentParams - textDocument : TextDocumentIdentifier - text : Maybe String -%runElab deriveJSON defaultOpts `{DidSaveTextDocumentParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose -public export -record DidCloseTextDocumentParams where - constructor MkDidCloseTextDocumentParams - textDocument : TextDocumentIdentifier -%runElab deriveJSON defaultOpts `{DidCloseTextDocumentParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose -public export -record TextDocumentSyncClientCapabilities where - constructor MkTextDocumentSyncClientCapabilities - dynamicRegistration : Maybe Bool - willSave : Maybe Bool - willSaveWaitUntil : Maybe Bool - didSave : Maybe Bool -%runElab deriveJSON defaultOpts `{TextDocumentSyncClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose -public export -record TextDocumentSyncOptions where - constructor MkTextDocumentSyncOptions - openClose : Maybe Bool - change : Maybe TextDocumentSyncKind - willSave : Maybe Bool - willSaveWaitUntil : Maybe Bool - save : Maybe (OneOf [Bool, SaveOptions]) -%runElab deriveJSON defaultOpts `{TextDocumentSyncOptions} diff --git a/src/Language/LSP/Message/Trace.idr b/src/Language/LSP/Message/Trace.idr deleted file mode 100644 index bed7e22..0000000 --- a/src/Language/LSP/Message/Trace.idr +++ /dev/null @@ -1,42 +0,0 @@ -module Language.LSP.Message.Trace - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -namespace Trace - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#traceValue - public export - data Trace = TraceOff | TraceMessages | TraceVerbose - -export -ToJSON Trace where - toJSON TraceOff = JString "off" - toJSON TraceMessages = JString "messages" - toJSON TraceVerbose = JString "verbose" - -export -FromJSON Trace where - fromJSON (JString "off") = pure TraceOff - fromJSON (JString "messages") = pure TraceMessages - fromJSON (JString "verbose") = pure TraceVerbose - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#setTrace -public export -record SetTraceParams where - constructor MkSetTraceParams - value : Trace -%runElab deriveJSON defaultOpts `{SetTraceParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#logTrace -public export -record LogTraceParams where - constructor MkLogTraceParams - message : String - verbose : Maybe String -%runElab deriveJSON defaultOpts `{LogTraceParams} diff --git a/src/Language/LSP/Message/URI.idr b/src/Language/LSP/Message/URI.idr deleted file mode 100644 index 20f9ab5..0000000 --- a/src/Language/LSP/Message/URI.idr +++ /dev/null @@ -1,33 +0,0 @@ -module Language.LSP.Message.URI - -import Data.Either -import Data.String.Parser -import public Data.URI -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Utils - -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#uri -public export -DocumentURI : Type -DocumentURI = URI - -export -ToJSON URI where - toJSON = JString . show - -export covering -FromJSON URI where - fromJSON (JString str) = eitherToMaybe (fst <$> parse (uriParser <* eos) str) - fromJSON _ = neutral - -export -ToJSON v => ToJSON (SortedMap URI v) where - toJSON m = JObject (map (mapFst show) $ toList $ toJSON <$> m) - -export covering -FromJSON v => FromJSON (SortedMap URI v) where - fromJSON (JObject xs) = fromList <$> traverse (\(k, v) => (,) <$> fromJSON (JString k) <*> fromJSON v) xs - fromJSON _ = neutral diff --git a/src/Language/LSP/Message/Utils.idr b/src/Language/LSP/Message/Utils.idr deleted file mode 100644 index b5beedc..0000000 --- a/src/Language/LSP/Message/Utils.idr +++ /dev/null @@ -1,85 +0,0 @@ -||| Common types and instances for JSON interoperability. -||| -||| (C) The Idris Community, 2021 -module Language.LSP.Message.Utils - -import public Data.OneOf -import Language.JSON -import Language.JSON.Interfaces -import Language.LSP.Message.Derive - -%default total - -public export -Eq JSON where - JNull == JNull = True - (JBoolean x) == (JBoolean y) = x == y - (JNumber x) == (JNumber y) = x == y - (JString x) == (JString y) = x == y - (JArray xs) == (JArray ys) = assert_total $ xs == ys - (JObject xs) == (JObject ys) = assert_total $ xs == ys - _ == _ = False - -||| Singleton type that models `null` in JSON. -public export -data Null = MkNull - -public export -Eq Null where - MkNull == MkNull = True - -public export -Ord Null where - compare MkNull MkNull = EQ - -public export -Show Null where - show MkNull = "null" - -export -ToJSON Null where - toJSON MkNull = JNull - -export -FromJSON Null where - fromJSON JNull = pure MkNull - fromJSON _ = neutral - -||| Converts an `UntaggedEither` value to the isomorphic value in `Either`. -public export -toEither : OneOf [a, b] -> Either a b -toEither (Here x) = Left x -toEither (There (Here x)) = Right x - -||| Converts an `Either` value to the isomorphic value in `UntaggedEither`. -public export -fromEither : Either a b -> OneOf [a, b] -fromEither (Left x) = make x -fromEither (Right x) = make x - -public export -toMaybe : OneOf [a, Null] -> Maybe a -toMaybe (Here x) = Just x -toMaybe (There (Here MkNull)) = Nothing - -public export -fromMaybe : Maybe a -> OneOf [a, Null] -fromMaybe (Just x) = make x -fromMaybe Nothing = make MkNull - -public export -ConstraintList : (Type -> Type) -> List Type -> Type -ConstraintList f [] = () -ConstraintList f (x :: xs) = (f x, ConstraintList f xs) - -export -ConstraintList ToJSON as => ToJSON (OneOf as) where - toJSON (Here x) = toJSON x - toJSON (There x) = toJSON x - -export -{as : _} -> ConstraintList FromJSON as => FromJSON (OneOf as) where - -- NOTE: The rightmost type is parsed first, since in the LSP specification - -- the most specific type appears also rightmost. - fromJSON {as = []} @{()} v = Nothing - fromJSON {as = (x :: xs)} @{(c, cs)} v = (There <$> fromJSON v) <|> (Here <$> fromJSON v) diff --git a/src/Language/LSP/Message/Window.idr b/src/Language/LSP/Message/Window.idr deleted file mode 100644 index ccf0ad4..0000000 --- a/src/Language/LSP/Message/Window.idr +++ /dev/null @@ -1,117 +0,0 @@ -module Language.LSP.Message.Window - -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -namespace MessageType - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage - public export - data MessageType = Error | Warning | Info | Log - -export -ToJSON MessageType where - toJSON Error = JNumber 1 - toJSON Warning = JNumber 2 - toJSON Info = JNumber 3 - toJSON Log = JNumber 4 - -export -FromJSON MessageType where - fromJSON (JNumber 1) = pure Error - fromJSON (JNumber 2) = pure Warning - fromJSON (JNumber 3) = pure Info - fromJSON (JNumber 4) = pure Log - fromJSON _ = Nothing - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage -public export -record ShowMessageParams where - constructor MkShowMessageParams - type : MessageType - message : String -%runElab deriveJSON defaultOpts `{ShowMessageParams} - -namespace ShowMessageRequestClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage - public export - record ShowMessageActionItem where - constructor MkShowMessageActionItem - additionalPropertiesSupport : Maybe Bool - %runElab deriveJSON defaultOpts `{ShowMessageActionItem} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage -public export -record ShowMessageRequestClientCapabilities where - constructor MkShowMessageRequestClientCapabilities - messageActionItem : Maybe ShowMessageActionItem -%runElab deriveJSON defaultOpts `{ShowMessageRequestClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage -public export -record MessageActionItem where - constructor MkMessageActionItem - title : String -%runElab deriveJSON defaultOpts `{MessageActionItem} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage -public export -record ShowMessageRequestParams where - constructor MkShowMessageRequestParams - type : MessageType - message : String - actions : Maybe (List MessageActionItem) -%runElab deriveJSON defaultOpts `{ShowMessageRequestParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument -public export -record ShowDocumentClientCapabilities where - constructor MkShowDocumentClientCapabilities - support : Bool -%runElab deriveJSON defaultOpts `{ShowDocumentClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument -public export -record ShowDocumentParams where - constructor MkShowDocumentParams - uri : URI - external_ : Maybe Bool - takeFocus : Maybe Bool - selection : Maybe Range -%runElab deriveJSON ({renames := [("external_", "external")]} defaultOpts) `{ShowDocumentParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument -public export -record ShowDocumentResult where - constructor MkShowDocumentResult - success : Bool -%runElab deriveJSON defaultOpts `{ShowDocumentResult} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_logMessage -public export -record LogMessageParams where - constructor MkLogMessageParams - type : MessageType - message : String -%runElab deriveJSON defaultOpts `{LogMessageParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_create -public export -record WorkDoneProgressCreateParams where - constructor MkWorkDoneProgressCreateParams - token : ProgressToken -%runElab deriveJSON defaultOpts `{WorkDoneProgressCreateParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_cancel -public export -record WorkDoneProgressCancelParams where - constructor MkWorkDoneProgressCancelParams - token : ProgressToken -%runElab deriveJSON defaultOpts `{WorkDoneProgressCancelParams} diff --git a/src/Language/LSP/Message/Workspace.idr b/src/Language/LSP/Message/Workspace.idr deleted file mode 100644 index 29feb8d..0000000 --- a/src/Language/LSP/Message/Workspace.idr +++ /dev/null @@ -1,472 +0,0 @@ -module Language.LSP.Message.Workspace - -import Data.SortedMap -import Language.JSON -import Language.LSP.Message.Derive -import Language.LSP.Message.DocumentSymbols -import Language.LSP.Message.Location -import Language.LSP.Message.Progress -import Language.LSP.Message.TextDocument -import Language.LSP.Message.URI -import Language.LSP.Message.Utils -import Language.Reflection - -%language ElabReflection -%default total - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit -public export -record TextEdit where - constructor MkTextEdit - range : Range - newText : String -%runElab deriveJSON defaultOpts `{TextEdit} - -export -Eq TextEdit where - (MkTextEdit range1 newText1) == (MkTextEdit range2 newText2) = range1 == range2 && newText1 == newText2 - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit -public export -record ChangeAnnotation where - constructor MkChangeAnnotation - label : String - needsConfirmation : Maybe Bool - description : Maybe String -%runElab deriveJSON defaultOpts `{ChangeAnnotation} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit -public export -ChangeAnnotationIdentifier : Type -ChangeAnnotationIdentifier = String - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit -public export -record AnnotatedTextEdit where - constructor MkAnnotatedTextEdit - range : Range - newText : String - annotationId : ChangeAnnotationIdentifier -%runElab deriveJSON defaultOpts `{AnnotatedTextEdit} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentEdit -public export -record TextDocumentEdit where - constructor MkTextDocumentEdit - textDocument : OptionalVersionedTextDocumentIdentifier - edits : List (OneOf [TextEdit, AnnotatedTextEdit]) -%runElab deriveJSON defaultOpts `{TextDocumentEdit} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion -public export -record InsertReplaceEdit where - constructor MkInsertReplaceEdit - newText : String - insert : Range - replace : Range -%runElab deriveJSON defaultOpts `{InsertReplaceEdit} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges -public export -record CreateFileOptions where - constructor MkCreateFileOptions - overwrite : Maybe Bool - ignoreIfExists : Maybe Bool -%runElab deriveJSON defaultOpts `{CreateFileOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges -public export -record RenameFileOptions where - constructor MkRenameFileOptions - overwrite : Maybe Bool - ignoreIfExists : Maybe Bool -%runElab deriveJSON defaultOpts `{RenameFileOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges -public export -record DeleteFileOptions where - constructor MkDeleteFileOptions - recursive : Maybe Bool - ignoreIfNotExists : Maybe Bool -%runElab deriveJSON defaultOpts `{DeleteFileOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges -public export -record CreateFile where - constructor MkCreateFile - uri : DocumentURI - options : Maybe CreateFileOptions - annotationId : ChangeAnnotationIdentifier -%runElab deriveJSON ({staticFields := [("kind", JString "create")]} defaultOpts) `{CreateFile} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges -public export -record RenameFile where - constructor MkRenameFile - oldUri : DocumentURI - newUri : DocumentURI - options : Maybe RenameFileOptions - annotationId : ChangeAnnotationIdentifier -%runElab deriveJSON ({staticFields := [("kind", JString "rename")]} defaultOpts) `{RenameFile} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges -public export -record DeleteFile where - constructor MkDeleteFile - uri : DocumentURI - options : Maybe DeleteFileOptions - annotationId : ChangeAnnotationIdentifier -%runElab deriveJSON ({staticFields := [("kind", JString "delete")]} defaultOpts) `{DeleteFile} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEdit -public export -record WorkspaceEdit where - constructor MkWorkspaceEdit - changes : Maybe (SortedMap DocumentURI (List TextEdit)) - documentChanges : Maybe (List (OneOf [TextDocumentEdit, CreateFile, RenameFile, DeleteFile])) - changeAnnotations : Maybe (SortedMap String ChangeAnnotation) -%runElab deriveJSON defaultOpts `{WorkspaceEdit} - -namespace ResourceOperationKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities - public export - data ResourceOperationKind = Create | Rename | Delete - -export -ToJSON ResourceOperationKind where - toJSON Create = JString "create" - toJSON Rename = JString "rename" - toJSON Delete = JString "delete" - -export -FromJSON ResourceOperationKind where - fromJSON (JString "create") = pure Create - fromJSON (JString "rename") = pure Rename - fromJSON (JString "delete") = pure Delete - fromJSON _ = neutral - -namespace FailureHandlingKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities - public export - data FailureHandlingKind = Abort | Transactional | Undo | TextOnlyTransactional - -export -ToJSON FailureHandlingKind where - toJSON Abort = JString "abort" - toJSON Transactional = JString "transactional" - toJSON Undo = JString "undo" - toJSON TextOnlyTransactional = JString "textOnlyTransactional" - -export -FromJSON FailureHandlingKind where - fromJSON (JString "abort") = pure Abort - fromJSON (JString "transactional") = pure Transactional - fromJSON (JString "undo") = pure Undo - fromJSON (JString "textOnlyTransactional") = pure TextOnlyTransactional - fromJSON _ = neutral - -namespace WorkspaceEditClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities - public export - record ChangeAnnotationSupport where - constructor MkChangeAnnotationSupport - groupsOnLabel : Maybe Bool - %runElab deriveJSON defaultOpts `{ChangeAnnotationSupport} - - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities -public export -record WorkspaceEditClientCapabilities where - constructor MkWorkspaceEditClientCapabilities - documentChanges : Maybe Bool - resourceOperations : Maybe (List ResourceOperationKind) - failureHandling : Maybe FailureHandlingKind - normalizesLineEndings : Maybe Bool - changeAnnotationSupport : Maybe ChangeAnnotationSupport -%runElab deriveJSON defaultOpts `{WorkspaceEditClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders -public export -record WorkspaceFoldersServerCapabilities where - constructor MkWorkspaceFoldersServerCapabilities - supported : Maybe Bool - changeNotifications : Maybe (OneOf [String, Bool]) -%runElab deriveJSON defaultOpts `{WorkspaceFoldersServerCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders -public export -record WorkspaceFolder where - constructor MkWorkspaceFolder - uri : DocumentURI - name : String -%runElab deriveJSON defaultOpts `{WorkspaceFolder} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders -public export -interface WorkspaceFoldersChangeEvent where - added : List WorkspaceFolder; - removed : List WorkspaceFolder; -%runElab deriveJSON defaultOpts `{WorkspaceFoldersChangeEvent} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders -public export -record DidChangeWorkspaceFoldersParams where - constructor MkDidChangeWorkspaceFoldersParams - event : WorkspaceFoldersChangeEvent -%runElab deriveJSON defaultOpts `{DidChangeWorkspaceFoldersParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration -public export -record DidChangeConfigurationClientCapabilities where - constructor MkDidChangeConfigurationClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{DidChangeConfigurationClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration -public export -record DidChangeConfigurationParams where - constructor MkDidChangeConfigurationParams - settings : JSON -%runElab deriveJSON defaultOpts `{DidChangeConfigurationParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration -public export -record ConfigurationItem where - constructor MkConfigurationItem - scopeUri : Maybe DocumentURI; - section : Maybe String -%runElab deriveJSON defaultOpts `{ConfigurationItem} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration -public export -record ConfigurationParams where - constructor MkConfigurationParams - items : List ConfigurationItem -%runElab deriveJSON defaultOpts `{ConfigurationParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles -public export -record DidChangeWatchedFilesClientCapabilities where - constructor MkDidChangeWatchedFilesClientCapabilities - dynamicRegistration : Maybe Bool -%runElab deriveJSON defaultOpts `{DidChangeWatchedFilesClientCapabilities} - -namespace WatchKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles - public export - data WatchKind = Create | Change | Delete - -watchKindToBits8 : WatchKind -> Bits8 -watchKindToBits8 Create = 1 -watchKindToBits8 Change = 2 -watchKindToBits8 Delete = 4 - -export -ToJSON (List WatchKind) where - toJSON = toJSON . foldr (prim__or_Bits8 . watchKindToBits8) 0 - -export -FromJSON (List WatchKind) where - fromJSON (JNumber x) = pure $ filter ((/=) 0 . prim__and_Bits8 (cast $ cast {to = Integer} x) . watchKindToBits8) [Create, Change, Delete] - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles -public export -record FileSystemWatcher where - constructor MkFileSystemWatcher - globPattern : String - kind : Maybe (List WatchKind) -%runElab deriveJSON defaultOpts `{FileSystemWatcher} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles -public export -record DidChangeWatchedFilesRegistrationOptions where - constructor MkDidChangeWatchedFilesRegistrationOptions - watchers : List FileSystemWatcher -%runElab deriveJSON defaultOpts `{DidChangeWatchedFilesRegistrationOptions} - -namespace FileChangeType - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles - public export - data FileChangeType = Created | Changed | Deleted - -export -ToJSON FileChangeType where - toJSON Created = JNumber 1 - toJSON Changed = JNumber 2 - toJSON Deleted = JNumber 3 - -export -FromJSON FileChangeType where - fromJSON (JNumber 1) = pure Created - fromJSON (JNumber 2) = pure Changed - fromJSON (JNumber 3) = pure Deleted - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles -public export -record FileEvent where - constructor MkFileEvent - uri : DocumentURI - type : FileChangeType -%runElab deriveJSON defaultOpts `{FileEvent} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles -public export -record DidChangeWatchedFilesParams where - constructor MkDidChangeWatchedFilesParams - changes : List FileEvent -%runElab deriveJSON defaultOpts `{DidChangeWatchedFilesParams} - -namespace WorkspaceSymbolClientCapabilities - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol - public export - record SymbolKindClientCapabilities where - constructor MkSymbolKindClientCapabilities - valueSet : Maybe (List SymbolKind) - %runElab deriveJSON defaultOpts `{SymbolKindClientCapabilities} - - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol - public export - record TagSupportClientCapabilities where - constructor MkTagSupportClientCapabilities - valueSet : List SymbolTag - %runElab deriveJSON defaultOpts `{TagSupportClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol -public export -record WorkspaceSymbolClientCapabilities where - constructor MkWorkspaceSymbolClientCapabilities - dynamicRegistration : Maybe Bool - symbolKind : Maybe SymbolKindClientCapabilities - tagSupport : TagSupportClientCapabilities -%runElab deriveJSON defaultOpts `{WorkspaceSymbolClientCapabilities} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol -public export -record WorkspaceSymbolOptions where - constructor MkWorkspaceSymbolOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{WorkspaceSymbolOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol -public export -record WorkspaceSymbolRegistrationOptions where - constructor MkWorkspaceSymbolRegistrationOptions - workDoneProgress : Maybe Bool -%runElab deriveJSON defaultOpts `{WorkspaceSymbolRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol -public export -record WorkspaceSymbolParams where - constructor MkWorkspaceSymbolParams - partialResultToken : Maybe ProgressToken - query : String -%runElab deriveJSON defaultOpts `{WorkspaceSymbolParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit -public export -record ApplyWorkspaceEditParams where - constructor MkApplyWorkspaceEditParams - label : Maybe String - edit : WorkspaceEdit -%runElab deriveJSON defaultOpts `{ApplyWorkspaceEditParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit -public export -record ApplyWorkspaceEditResponse where - constructor MkApplyWorkspaceEditResponse - applied : Bool - failureReason : Maybe String - failedChange : Maybe Integer -%runElab deriveJSON defaultOpts `{ApplyWorkspaceEditResponse} - -namespace FileOperationPatternKind - ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles - public export - data FileOperationPatternKind = FileKind | FolderKind - -export -ToJSON FileOperationPatternKind where - toJSON FileKind = JString "file" - toJSON FolderKind = JString "folder" - -export -FromJSON FileOperationPatternKind where - fromJSON (JString "file") = pure FileKind - fromJSON (JString "folder") = pure FolderKind - fromJSON _ = neutral - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles -public export -record FileOperationPatternOptions where - constructor MkFileOperationPatternOptions - ignoreCase : Maybe Bool -%runElab deriveJSON defaultOpts `{FileOperationPatternOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles -public export -record FileOperationPattern where - constructor MkFileOperationPattern - glob : String - matches : Maybe FileOperationPatternKind - options : FileOperationPatternOptions -%runElab deriveJSON defaultOpts `{FileOperationPattern} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles -public export -record FileOperationFilter where - constructor MkFileOperationFilter - scheme : Maybe String - pattern : FileOperationPattern -%runElab deriveJSON defaultOpts `{FileOperationFilter} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles -public export -record FileOperationRegistrationOptions where - constructor MkFileOperationRegistrationOptions - filters : List FileOperationFilter -%runElab deriveJSON defaultOpts `{FileOperationRegistrationOptions} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles -public export -record FileCreate where - constructor MkFileCreate - uri : URI -%runElab deriveJSON defaultOpts `{FileCreate} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles -public export -record CreateFilesParams where - constructor MkCreateFilesParams - files : List FileCreate -%runElab deriveJSON defaultOpts `{CreateFilesParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles -public export -record FileRename where - constructor MkFileRename - oldUri : URI - newUri : URI -%runElab deriveJSON defaultOpts `{FileRename} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles -public export -record RenameFilesParams where - constructor MkRenameFilesParams - files : List FileRename -%runElab deriveJSON defaultOpts `{RenameFilesParams} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles -public export -record FileDelete where - constructor MkFileDelete - uri : URI -%runElab deriveJSON defaultOpts `{FileDelete} - -||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles -public export -record DeleteFilesParams where - constructor MkDeleteFilesParams - files : List FileDelete -%runElab deriveJSON defaultOpts `{DeleteFilesParams} diff --git a/src/Server/Configuration.idr b/src/Server/Configuration.idr index 7c5944f..a295f1a 100644 --- a/src/Server/Configuration.idr +++ b/src/Server/Configuration.idr @@ -19,7 +19,7 @@ import Language.LSP.Message.Initialize import Language.LSP.Message.Location import Language.LSP.Message.SemanticTokens import Language.LSP.Message.URI -import Server.Severity +import Language.LSP.Severity import System.File import Data.String import Data.List1 diff --git a/src/Server/Diagnostics.idr b/src/Server/Diagnostics.idr index 0d893bf..18e09fa 100644 --- a/src/Server/Diagnostics.idr +++ b/src/Server/Diagnostics.idr @@ -16,6 +16,7 @@ import Idris.Syntax import Idris.Doc.String import Language.JSON import Language.LSP.Message +import Language.LSP.Utils import Libraries.Data.String.Extra import Parser.Support import Server.Configuration diff --git a/src/Server/Log.idr b/src/Server/Log.idr index 97b795a..2f4a7c6 100644 --- a/src/Server/Log.idr +++ b/src/Server/Log.idr @@ -7,7 +7,7 @@ import Core.Context.Context import Core.Core import Core.Directory import Server.Configuration -import Server.Severity +import Language.LSP.Severity import Server.Utils import System.Directory import System.File diff --git a/src/Server/Main.idr b/src/Server/Main.idr index f54813a..adc1a09 100644 --- a/src/Server/Main.idr +++ b/src/Server/Main.idr @@ -22,6 +22,7 @@ import Idris.Version import IdrisPaths import Language.JSON import Language.LSP.Message +import Language.LSP.Utils import Libraries.Utils.Path import Server.Configuration import Server.Log @@ -60,7 +61,7 @@ parseHeader str = parseHeaderPart : (h : File) -> Core (Either FileError (Maybe Int)) parseHeaderPart h = do - Right line <- fGetHeader h + Right line <- coreLift $ fGetHeader h | Left err => pure $ Left err case parseHeader line of Just (ContentLength l) => parseHeaderPart h *> pure (Right (Just l)) diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index 6500d08..bd7dd9a 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -48,6 +48,9 @@ import Language.LSP.DocumentSymbol import Language.LSP.Message import Language.LSP.Metavars import Language.LSP.SignatureHelp +import Language.LSP.VirtualDocument +import Language.LSP.Utils +import Language.LSP.Severity import Libraries.Data.List.Extra import Libraries.Data.PosMap import Libraries.Data.String.Extra @@ -61,9 +64,7 @@ import Server.Log import Server.QuickFix import Server.Response import Server.SemanticTokens -import Server.Severity import Server.Utils -import Server.VirtualDocument import System import System.Clock import System.Directory diff --git a/src/Server/Response.idr b/src/Server/Response.idr index c78cbe8..8d8fc28 100644 --- a/src/Server/Response.idr +++ b/src/Server/Response.idr @@ -15,6 +15,7 @@ import Idris.Resugar import Idris.Syntax import Language.JSON import Language.LSP.Message +import Language.LSP.Utils import Parser.Support import Server.Configuration import Server.Diagnostics diff --git a/src/Server/Severity.idr b/src/Server/Severity.idr deleted file mode 100644 index e0748d5..0000000 --- a/src/Server/Severity.idr +++ /dev/null @@ -1,56 +0,0 @@ -||| Logging utilities for the LSP server implementation. -||| -||| (C) The Idris Community, 2023 -module Server.Severity - -import Data.String - -%default total - -||| Type for the severity of logging messages. -||| Levels are roughly categorised as follow: -||| - Debug Messages targeted only for developing purposes -||| - Info Messages for progress without unexpected behaviour or errors -||| - Warning Messages for unsupported requests or wrong configurations -||| - Error Messages for either server or compiler error which are unexpected but recoverable -||| - Critical Messages for error that require immediate stopping of the server -public export -data Severity = Debug | Info | Warning | Error | Critical - -export -parseSeverity : String -> Maybe Severity -parseSeverity str = case toUpper str of - "DEBUG" => Just Debug - "INFO" => Just Info - "WARNING" => Just Warning - "ERROR" => Just Error - "CRITICAL" => Just Critical - _ => Nothing - -Cast Severity Integer where - cast Debug = 0 - cast Info = 1 - cast Warning = 2 - cast Error = 3 - cast Critical = 4 - -export -Eq Severity where - Debug == Debug = True - Info == Info = True - Warning == Warning = True - Error == Error = True - Critical == Critical = True - _ == _ = False - -export -Show Severity where - show Debug = "DEBUG" - show Info = "INFO" - show Warning = "WARNING" - show Error = "ERROR" - show Critical = "CRITICAL" - -export -Ord Severity where - compare x y = compare (cast {to = Integer} x) (cast y) diff --git a/src/Server/Utils.idr b/src/Server/Utils.idr index d220ade..007658e 100644 --- a/src/Server/Utils.idr +++ b/src/Server/Utils.idr @@ -32,134 +32,6 @@ uncons' : List a -> Maybe (a, List a) uncons' [] = Nothing uncons' (x :: xs) = Just (x, xs) -export -headerLineEnd : String -headerLineEnd = if isWindows then "\n" else "\r\n" - -||| Reads a single header from an LSP message on the supplied file handle. -||| Headers end with the string "\r\n". -export -fGetHeader : (handle : File) -> Core (Either FileError String) -fGetHeader handle = do - False <- coreLift $ fEOF handle - | True => coreLift $ exitWith (ExitFailure 1) - Right l <- coreLift $ fGetLine handle - | Left err => pure $ Left err - -- TODO: reading up to a string should probably be handled directly by the FFI primitive - -- or at least in a more efficient way in Idris2 - if isSuffixOf headerLineEnd l - then pure $ Right l - else (map (l ++)) <$> fGetHeader handle - --- From Language.JSON.Data -private -b16ToHexString : Bits16 -> String -b16ToHexString n = - case n of - 0 => "0" - 1 => "1" - 2 => "2" - 3 => "3" - 4 => "4" - 5 => "5" - 6 => "6" - 7 => "7" - 8 => "8" - 9 => "9" - 10 => "A" - 11 => "B" - 12 => "C" - 13 => "D" - 14 => "E" - 15 => "F" - other => assert_total $ - b16ToHexString (n `shiftR` 4) ++ - b16ToHexString (n .&. 15) - -||| Pad a string with leading zeros, if -||| its length is less than 4, up to 4 symbols. -pad4 : String -> String -pad4 str = - case length str of - 0 => "0000" - 1 => "000" ++ str - 2 => "00" ++ str - 3 => "0" ++ str - _ => str - -||| See https://en.wikipedia.org/wiki/UTF-16 for the algorithm. -||| Returns the codepoint value represented as a hex string, -||| if it encodes a symbol from the Basic Multilingual Plane. -||| Otherwise, returns the 16-bit surrogate pair, every element of which -||| is, in turn, represented as a hex string. -encodeCodepointH : Bits32 -> Either String (String, String) -encodeCodepointH x = - case x <= 0xFFFF of - -- Basic Multilingual Plane - True => Left $ pad4 (b16ToHexString (cast x)) - -- One of the Supplementary Planes - False => - let x' = x - 0x10000 in - Right $ - ( pad4 (b16ToHexString (cast $ 0xD800 + (x' `shiftR` 10))) - , pad4 (b16ToHexString (cast $ 0xDC00 + (x' .&. 0b1111111111)))) - -||| Encode an arbitrary unicode codepointby escaping it -||| as defined in -||| https://tools.ietf.org/id/draft-ietf-json-rfc4627bis-09.html#rfc.section.7 -encodeCodepoint : Bits32 -> String -encodeCodepoint x = - case encodeCodepointH x of - Left w => "\\u" ++ w - Right (w1, w2) => "\\u" ++ w1 ++ "\\u" ++ w2 - -||| Here we escape all wide characters (exceeding 8 bit width). -||| JSON spec doesn't seem to require that, -||| but at least some of the editors (e.g. Neovim) expect -||| wide characters escaped, otherwise refusing to work. -private -showChar : Char -> String -showChar c = - case c of - '\b' => "\\b" - '\f' => "\\f" - '\n' => "\\n" - '\r' => "\\r" - '\t' => "\\t" - '\\' => "\\\\" - '"' => "\\\"" - c => if isControl c || c >= '\127' - then encodeCodepoint (cast $ ord c) - else singleton c - -private -showString : String -> String -showString x = "\"" ++ concatMap showChar (unpack x) ++ "\"" - -export -stringify : JSON -> String -stringify JNull = "null" -stringify (JBoolean x) = if x then "true" else "false" -stringify (JNumber x) = - let s = show x - in if isSuffixOf ".0" s then substr 0 (length s `minus` 2) s else s -stringify (JString x) = showString x -stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]" - where - stringifyValues : List JSON -> String - stringifyValues [] = "" - stringifyValues (x :: xs) = - stringify x ++ if isNil xs then "" else "," ++ stringifyValues xs -stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}" - where - stringifyProp : (String, JSON) -> String - stringifyProp (key, value) = showString key ++ ":" ++ stringify value - - stringifyProps : List (String, JSON) -> String - stringifyProps [] = "" - stringifyProps (x :: xs) = - stringifyProp x ++ if isNil xs then "" else "," ++ stringifyProps xs - export findInTreeLoc' : FilePos -> FilePos -> PosMap (NonEmptyFC, a) -> List (NonEmptyFC, a) findInTreeLoc' sp ep m = sortBy (\x, y => cmp (measure x) (measure y)) $ dominators (sp, ep) m @@ -237,42 +109,8 @@ searchCache r type = do let inRange = dominators (cast r) cache pure $ concatMap (snd . snd) $ filter (\(_, t, _) => type == t) inRange -export -pathToURI : String -> URI -pathToURI path = - MkURI { scheme = "file" - , authority = Just (MkURIAuthority Nothing "" Nothing) - , path = path - , query = "" - , fragment = "" - } - export toStart : FC -> FC toStart (MkFC f _ _) = MkFC f (0, 0) (0, 0) toStart (MkVirtualFC f _ _) = MkVirtualFC f (0, 0) (0, 0) toStart EmptyFC = EmptyFC - -export -Show Position where - show (MkPosition line character) = "\{show line}:\{show character}" - -export -Show Range where - show (MkRange start end) = "\{show start} -- \{show end}" - -export -systemPathToURIPath : String -> String -systemPathToURIPath p = if not isWindows then p else - let p1 = fastPack (map (\c => if c == '\\' then '/' else c) (fastUnpack p)) - in case strUncons p1 of - Just ('/', _) => p1 - _ => strCons '/' p1 - -export -uriPathToSystemPath : String -> String -uriPathToSystemPath p = if not isWindows then p else - let p1 = case strUncons p of - Just ('/', tail) => tail - _ => p - in fastPack (map (\c => if c == '/' then '\\' else c) (fastUnpack p1)) diff --git a/src/Server/VirtualDocument.idr b/src/Server/VirtualDocument.idr deleted file mode 100644 index ac83eae..0000000 --- a/src/Server/VirtualDocument.idr +++ /dev/null @@ -1,480 +0,0 @@ -module Server.VirtualDocument - --- The VirtualDocument is the version of the document that the LSP server maintains --- based on the incoming DidChange events. It should mirror the actively edited but --- unsaved content of the opened documents. - -import Data.Nat -import Data.List -import Data.String -import Data.OneOf -import Language.LSP.Message.Location -import Language.LSP.Message.TextDocument -import Decidable.Equality -import Data.DPair -import Control.Function -import Syntax.PreorderReasoning -import Data.Void - -%default total - - --- As the edits come in incremental change, the virtual document must be --- updated accordingly. The string needs to be split in a particular way, --- as detailed below: --- --- Cut the string in half. --- --- The `rangeSplit` cuts the string into three parts based on a Range. --- --- In a Range based edit, the client sends a text that must replace the part --- within the Range found in the edit request. The Range consists of a start --- and an end position. Positions consist of a line and a character index. --- --- Although the Position is encoded with line and char index, the file is --- represented as a String, in which a natural number indexes characters. --- The Position must be mapped to the string index-based encoding, which --- can be done via a string traversal. When a newline character is found, --- the line index is decreased. When the line index reaches zero, the character --- index is decreased. When the character index reaches zero, the string index of --- the Position is found. See below: --- --- ... m n p --- ...4567890123456789012345678901234567890.... (positions in string) --- ^ ^ --- start end (range in format (line:character)) --- --- As the text edit replaces a string in the Range, the prefix of the string --- must be kept. This means (0..start-1) both indexes included, then the new --- string must be inserted, and after the string from the end position must --- be included (end..length-1), both indexes included. --- --- Although the situation is complex, the position encoding is based on line --- and character index, which must be decreased appropriately; the new line --- encoding of \r\n vs \n makes it trickier. However, this module only handles \n case. --- --- Another complication is that the positions could refer to non-existing parts --- of the content. Such as, the Position could point after the end of --- the line end of the file. --- --- The [before the first character of the line] range is encoded as the start position --- pointing after the line's last character and at the new line's first character --- such as (l,c+1) and (l+1,0). --- --- Characters that point after the last character are considered invalid Range, --- and it must be interpreted as the last character of the line. - - -Pos : Type -Pos = (Nat, Nat) - -||| Line length as defined in LSP, newline character is not counted in. -||| -||| See more: -||| https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#position -lineLength : String -> Nat -lineLength "" = 0 -lineLength str = assert_total $ - let l = strLength str in - if isNL (strIndex str (l - 1)) - then minus (cast l) 1 - else cast l - --- Take the string up to the position, character addressed by the position is included. -takePos : Pos -> String -> String -takePos (l,c) str = - let ls : List String = lines str in - let ln : Nat = length ls in - case l < ln of - False => fastUnlines ls - True => - let (pre, post) = splitAt l ls in - case post of - [] => fastUnlines pre - (pl :: _) => - let ll : Nat := lineLength pl in - let cx : Nat := if c > ll then ll else c in - fastUnlines $ pre ++ [strSubstr 0 (cast cx) pl] - --- Drop the string up to the position, character addressed by the position is excluded. -dropPos : Pos -> String -> String -dropPos (l,c) str = - let ls : List String = lines str in - let ln : Nat = length ls in - case l < ln of - False => "\n" -- Assumes always a newline at the end. - True => - let (pre, post) = splitAt l ls in - case post of - [] => "\n" - (pl :: prest) => - let ll : Nat := lineLength pl in - let cx : Nat := if c > ll then ll else c in - fastUnlines $ (strSubstr (cast cx) (cast (minus (cast (strLength pl)) cx)) pl :: prest) - --- Newline character is always assumed from takePos and dropPos, and they must be --- removed to re-establish consistency. The SubString operations should be quick. -dropLastNL : String -> String -dropLastNL str = assert_total $ case strLength str of - 0 => str - n => strSubstr 0 (n - 1) str - --- Computes the pre and post part for the given range. Drops the part which is addressed by the range. -rangeSplit : Pos -> Pos -> String -> (String, String) -rangeSplit s e str = (dropLastNL $ takePos s str, dropLastNL $ dropPos e str) - -||| Updates the content string with the new string replacing the part between the start and end positions. -||| -||| This function is an approximation as the implementation is based on unlines and lines, -||| and the lines function adds newline characters. The edge-case around newlines -||| at the end of files is simplified to assume that the virtual content always -||| has the empty line as the last line. -update : Pos -> Pos -> String -> String -> String -update s e new content = - let (pre, post) = rangeSplit s e content in - fastConcat [pre, new, post, "\n"] - --- * Identifier - --- Oversimplified version of the identifier. -isIdentifierChar : Char -> Bool -isIdentifierChar c = or [isAlphaNum c, c == '.', c == '_', c == '\''] - --- * Word at position - --- Determines the identifier at the index. --- --- The implementation tart out scanning for the start position --- of the identifier and then looks for the end position. -identifierAtIndex : String -> Nat -> String -identifierAtIndex "" i = "" -identifierAtIndex str i = identifierPre (minus i 1) i - where - l : Nat - l = cast (strLength str) - - identifierPost : Nat -> Nat -> String - identifierPost n Z = assert_total $ case isIdentifierChar (strIndex str (cast Z)) of - True => identifierPost n (S Z) - False => "" -- n < m -- assumed and this means an empty result - identifierPost n (S m) = assert_total $ case (S m) == l of - True => strSubstr (cast n) (cast (minus (S m) n)) str - False => case isIdentifierChar (strIndex str (cast (S m))) of - True => identifierPost n (S (S m)) - False => strSubstr (cast n) (cast (minus (S m) n)) str - - identifierPre : Nat -> Nat -> String - identifierPre Z m = assert_total $ case isIdentifierChar (strIndex str (cast Z)) of - True => identifierPost Z m - False => identifierPost (S Z) m - identifierPre (S n) m = assert_total $ case isIdentifierChar (strIndex str (cast (S n))) of - True => identifierPre n m - False => identifierPost (S (S n)) m - --- Identifier at position. --- --- Picks the line and char, if exists, otherwise reports empty string. -identifierAtPos : Pos -> String -> String -identifierAtPos (l,c) str = - let ls : List String := lines str in - let ln : Nat := length ls in - case l > ln of - True => "" - False => case drop l ls of - [] => "" - (line::_) => - let ll : Nat := lineLength line in - let cx : Nat := if c > ll then ll else c in - identifierAtIndex line cx - -||| Determines an identifier like string at a given position. -||| -||| The empty String will be reported if the position points to a non-existent -||| part of the String. This function is needed when generating the suggestion list. -export -identifierAtPosition : Position -> String -> String -identifierAtPosition (MkPosition line character) str = identifierAtPos (cast line, cast character) str - --- * LSP API - -validRange : (startline, startchar, endline, endchar : Nat) -> Bool -validRange startline startchar endline endchar = - case compare startline endline of - LT => True - EQ => case compare startchar endchar of - LT => True - EQ => True - GT => False - GT => False - -changeRange : Range -> String -> String -> Either String String -changeRange (MkRange (MkPosition sl sc) (MkPosition el ec)) content str = - case validRange (cast sl) (cast sc) (cast el) (cast ec) of - False => Left "Invalid range: \{show (sl,sc,el,ec)}" - True => Right $ update (cast sl, cast sc) (cast el, cast ec) str content - -contentChangeEvent : TextDocumentContentChangeEvent -> String -contentChangeEvent (MkTextDocumentContentChangeEvent text) = text - -contentChangeEventWithRange : TextDocumentContentChangeEventWithRange -> String -> Either String String -contentChangeEventWithRange - (MkTextDocumentContentChangeEventWithRange range rangeLength text) - content - = changeRange range content text - -contentChangeOneOf : OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange] -> String -> Either String String -contentChangeOneOf (Here c) _ = Right $ contentChangeEvent c -contentChangeOneOf (There (Here r)) c = contentChangeEventWithRange r c - -export -changeVirtualContent - : List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange]) - -> String -> Either String String -changeVirtualContent changes content = foldlM (flip contentChangeOneOf) content changes - ---------------------------- --- Poor man's testing :) -- ---------------------------- - -wordPosTestCase : Pos -> String -> String -> IO () -wordPosTestCase p str expected = do - let res = identifierAtPos p str - if expected == res - then do - putStrLn "OK: identifierAtPos \{show p} \{show str} \{show expected}" - else do - putStrLn "Failed: identifierAtPos \{show p} \{show str} \{show expected}" - putStrLn "Expected: \{show expected}" - putStrLn "Got: \{show res}" - -updateTestCase : Pos -> Pos -> String -> String -> String -> IO () -updateTestCase s e new str expected = do - let res = update s e new str - if expected == res - then do - putStrLn "OK: update \{show s} \{show e} \{show new} \{show str}" - else do - putStrLn "Failed: update \{show s} \{show e} \{show new} \{show str}" - putStrLn "Expected: \{show expected}" - putStrLn "Got: \{show res}" - -tests : IO () -tests = do - - -- Update tests - - do -- Empty string - let str = "" - updateTestCase (0,0) (0,0) "" str "\n" - updateTestCase (0,0) (0,0) "a\nb" str "a\nb\n" - updateTestCase (0,0) (0,1) "a" str "a\n" - updateTestCase (1,0) (1,0) "a" str "a\n" - updateTestCase (1,1) (1,1) "a" str "a\n" - updateTestCase (1,1) (1,2) "a" str "a\n" - updateTestCase (1,1) (2,2) "a" str "a\n" - - do -- New line sting - let str = " " - updateTestCase (0,0) (0,0) "" str " \n" - updateTestCase (0,0) (0,0) "a\nb" str "a\nb \n" - updateTestCase (0,0) (0,1) "a" str "a\n" - updateTestCase (1,0) (1,0) "a" str " a\n" - updateTestCase (1,1) (1,1) "a" str " a\n" - updateTestCase (2,1) (2,1) "" str " \n" - updateTestCase (2,1) (2,1) "a" str " a\n" - - do -- New line sting - let str = "\n" - updateTestCase (0,0) (0,0) "" str "\n" - updateTestCase (0,0) (0,0) "a\nb" str "a\nb\n" - updateTestCase (0,0) (0,1) "a" str "a\n" - updateTestCase (1,0) (1,0) "a" str "a\n" - updateTestCase (1,1) (1,1) "a" str "a\n" - updateTestCase (2,1) (2,1) "" str "\n" - updateTestCase (2,1) (2,1) "a" str "a\n" - - do -- One line, no newline - -- 0 1 1 - -- 012345678901234 - let str = "This is a line." - updateTestCase (0,0) (0,0) "" str "This is a line.\n" - updateTestCase (0,5) (0,5) "" str "This is a line.\n" - updateTestCase (0,0) (0,0) "a" str "aThis is a line.\n" - updateTestCase (0,5) (0,5) "a" str "This ais a line.\n" - updateTestCase (0,5) (0,8) "xx" str "This xxa line.\n" - updateTestCase (0,5) (0,15) "aaa" str "This aaa\n" - updateTestCase (0,3) (0,4) "" str "Thi is a line.\n" - updateTestCase (0,11) (0,20) "" str "This is a l\n" - - do -- One line, newline - -- 0 1 1 - -- 0123456789012345678 - let str = "This is a newline.\n" - updateTestCase (0,0) (0,0) "" str str - updateTestCase (0,5) (0,5) "" str str - updateTestCase (0,0) (0,0) "a" str "aThis is a newline.\n" - updateTestCase (0,5) (0,5) "a" str "This ais a newline.\n" - updateTestCase (0,5) (0,8) "aa" str "This aaa newline.\n" - updateTestCase (0,5) (0,18) "aaa" str "This aaa\n" - updateTestCase (0,18) (0,18) "a" str "This is a newline.a\n" - updateTestCase (0,11) (0,20) "" str "This is a n\n" - - do -- Multiple lines, no newline at the last line. - -- 0 1 2 2 0 1 2 2 0 1 2 2 - -- 012345678901234567890123 0123456789012345678901234 01234567890123456789012 - let str = "This is the first line.\nThis is the second line.\nThis is the third line." - updateTestCase (1,0) (1,0) "" str (str ++ "\n") - updateTestCase (1,0) (1,0) "a" str "This is the first line.\naThis is the second line.\nThis is the third line.\n" - -- https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#range - -- If you want to specify a range that contains a line including the line ending character(s) - -- then use an end position denoting the start of the next line. - updateTestCase (1,24) (2,0) "a" str "This is the first line.\nThis is the second line.aThis is the third line.\n" - updateTestCase (1,19) (2,0) "a" str "This is the first line.\nThis is the second aThis is the third line.\n" - updateTestCase (1,0) (2,0) "" str "This is the first line.\nThis is the third line.\n" - updateTestCase (1,0) (2,0) "a" str "This is the first line.\naThis is the third line.\n" - updateTestCase (1,8) (2,8) "" str "This is the first line.\nThis is the third line.\n" - updateTestCase (1,8) (2,8) "a " str "This is the first line.\nThis is a the third line.\n" - updateTestCase (1,8) (2,9) "x" str "This is the first line.\nThis is xhe third line.\n" - updateTestCase (1,23) (2,22) "" str "This is the first line.\nThis is the second line.\n" - updateTestCase (1,23) (2,22) "a" str "This is the first line.\nThis is the second linea.\n" - updateTestCase (1,23) (2,23) "a" str "This is the first line.\nThis is the second linea\n" - updateTestCase (0,23) (1,24) "" str "This is the first line.\nThis is the third line.\n" - updateTestCase (1,0) (1,40) "" str "This is the first line.\n\nThis is the third line.\n" - updateTestCase (1,0) (1,24) "" str "This is the first line.\n\nThis is the third line.\n" - updateTestCase (1,10) (1,40) "" str "This is the first line.\nThis is th\nThis is the third line.\n" - updateTestCase (1,0) (4,40) "" str "This is the first line.\n\n" - updateTestCase (1,10) (4,40) "" str "This is the first line.\nThis is th\n" - - do -- Multiple lines, newline at the last line. - -- 0 1 2 0 1 2 2 0 1 2 2 - -- 012345678901234567890123 0123456789012345678901234 012345678901234567890123 - let str = "This is the first line.\nThis is the second line.\nThis is the third line.\n" - updateTestCase (1,0) (1,0) "" str str - updateTestCase (1,0) (1,0) "a" str "This is the first line.\naThis is the second line.\nThis is the third line.\n" - -- https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#range - -- If you want to specify a range that contains a line including the line ending character(s) - -- then use an end position denoting the start of the next line. - updateTestCase (1,24) (2,0) "a" str "This is the first line.\nThis is the second line.aThis is the third line.\n" - updateTestCase (1,19) (2,0) "a" str "This is the first line.\nThis is the second aThis is the third line.\n" - updateTestCase (1,0) (2,0) "" str "This is the first line.\nThis is the third line.\n" - updateTestCase (1,0) (2,0) "a" str "This is the first line.\naThis is the third line.\n" - updateTestCase (1,8) (2,8) "" str "This is the first line.\nThis is the third line.\n" - updateTestCase (1,8) (2,8) "a " str "This is the first line.\nThis is a the third line.\n" - updateTestCase (1,8) (2,9) "x" str "This is the first line.\nThis is xhe third line.\n" - updateTestCase (1,23) (2,22) "" str "This is the first line.\nThis is the second line.\n" - updateTestCase (1,23) (2,22) "a" str "This is the first line.\nThis is the second linea.\n" - updateTestCase (1,23) (2,23) "a" str "This is the first line.\nThis is the second linea\n" - updateTestCase (0,23) (1,24) "" str "This is the first line.\nThis is the third line.\n" - updateTestCase (1,0) (1,40) "" str "This is the first line.\n\nThis is the third line.\n" - updateTestCase (1,0) (1,24) "" str "This is the first line.\n\nThis is the third line.\n" - updateTestCase (1,10) (1,40) "" str "This is the first line.\nThis is th\nThis is the third line.\n" - updateTestCase (1,0) (4,40) "" str "This is the first line.\n\n" - updateTestCase (1,10) (4,40) "" str "This is the first line.\nThis is th\n" - - -- Word at position tests. - - do -- Empty string - wordPosTestCase (0,0) "" "" - wordPosTestCase (0,10) "" "" - wordPosTestCase (1,0) "" "" - wordPosTestCase (1,10) "" "" - - do -- New line - wordPosTestCase (0,0) "\n" "" - wordPosTestCase (0,10) "\n" "" - wordPosTestCase (1,0) "\n" "" - wordPosTestCase (1,10) "\n" "" - wordPosTestCase (2,0) "\n" "" - wordPosTestCase (2,10) "\n" "" - - do -- Space character - wordPosTestCase (0,0) " " "" - wordPosTestCase (0,10) " " "" - wordPosTestCase (1,0) " " "" - wordPosTestCase (1,10) " " "" - - do -- One line without newline - -- 0 1 1 - -- 012345678901234 - let str = "This is a line." - wordPosTestCase (0,0) str "This" - wordPosTestCase (0,2) str "This" - wordPosTestCase (0,4) str "This" - wordPosTestCase (0,5) str "is" - wordPosTestCase (0,6) str "is" - wordPosTestCase (0,7) str "is" - wordPosTestCase (0,8) str "a" - wordPosTestCase (0,9) str "a" - wordPosTestCase (0,10) str "line." - wordPosTestCase (0,12) str "line." - wordPosTestCase (0,14) str "line." - wordPosTestCase (0,20) str "line." - wordPosTestCase (1,0) str "" - - do -- One line with newline - -- 0 1 1 - -- 0123456789012345 - let str = "This is a line.\n" - wordPosTestCase (0,0) str "This" - wordPosTestCase (0,2) str "This" - wordPosTestCase (0,4) str "This" - wordPosTestCase (0,5) str "is" - wordPosTestCase (0,6) str "is" - wordPosTestCase (0,7) str "is" - wordPosTestCase (0,8) str "a" - wordPosTestCase (0,9) str "a" - wordPosTestCase (0,10) str "line." - wordPosTestCase (0,12) str "line." - wordPosTestCase (0,14) str "line." - wordPosTestCase (0,20) str "line." - wordPosTestCase (1,0) str "" - - do -- Three lines without newline - -- 0 1 2 0 1 2 2 0 1 2 2 - -- 012345678901234567890123 0123456789012345678901234 01234567890123456789012 - let str = "This is the first line.\nThis is the second line.\nThis is the third line." - wordPosTestCase (0,0) str "This" - wordPosTestCase (0,2) str "This" - wordPosTestCase (0,4) str "This" - wordPosTestCase (0,5) str "is" - wordPosTestCase (0,6) str "is" - wordPosTestCase (0,7) str "is" - wordPosTestCase (0,8) str "the" - wordPosTestCase (0,12) str "first" - wordPosTestCase (0,21) str "line." - wordPosTestCase (0,30) str "line." - wordPosTestCase (1,0) str "This" - wordPosTestCase (1,14) str "second" - wordPosTestCase (1,21) str "line." - wordPosTestCase (1,30) str "line." - wordPosTestCase (2,0) str "This" - wordPosTestCase (2,14) str "third" - wordPosTestCase (2,21) str "line." - wordPosTestCase (2,30) str "line." - wordPosTestCase (3,0) str "" - wordPosTestCase (3,30) str "" - - do -- Three lines with newline - -- 0 1 2 0 1 2 2 0 1 2 2 - -- 012345678901234567890123 0123456789012345678901234 012345678901234567890123 - let str = "This is the first line.\nThis is the second line.\nThis is the third line.\n" - wordPosTestCase (0,0) str "This" - wordPosTestCase (0,2) str "This" - wordPosTestCase (0,4) str "This" - wordPosTestCase (0,5) str "is" - wordPosTestCase (0,6) str "is" - wordPosTestCase (0,7) str "is" - wordPosTestCase (0,8) str "the" - wordPosTestCase (0,12) str "first" - wordPosTestCase (0,21) str "line." - wordPosTestCase (0,30) str "line." - wordPosTestCase (1,0) str "This" - wordPosTestCase (1,14) str "second" - wordPosTestCase (1,21) str "line." - wordPosTestCase (1,30) str "line." - wordPosTestCase (2,0) str "This" - wordPosTestCase (2,14) str "third" - wordPosTestCase (2,21) str "line." - wordPosTestCase (2,30) str "line." - wordPosTestCase (3,0) str "" - wordPosTestCase (3,30) str ""