0 | module Language.LSP.Message.Initialize
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.ClientCapabilities
 4 | import Language.LSP.Message.Derive
 5 | import Language.LSP.Message.Progress
 6 | import Language.LSP.Message.ServerCapabilities
 7 | import Language.LSP.Message.Trace
 8 | import Language.LSP.Message.URI
 9 | import Language.LSP.Message.Utils
10 | import Language.LSP.Message.Workspace
11 | import Language.Reflection
12 |
13 | %language ElabReflection
14 | %default total
15 |
16 | namespace InitializeParams
17 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
18 |   public export
19 |   record ClientInfo where
20 |     name    : String
21 |     version : Maybe String
22 |   %runElab deriveJSON defaultOpts `{ClientInfo}
23 |
24 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
25 | public export
26 | record InitializeParams where
27 |   constructor MkInitializeParams
28 |   processId             : OneOf [Integer, Null]
29 |   clientInfo            : Maybe ClientInfo
30 |   locale                : Maybe String
31 |   rootPath              : Maybe (OneOf [String, Null])
32 |   rootUri               : OneOf [URI, Null]
33 |   initializationOptions : Maybe JSON
34 |   capabilities          : ClientCapabilities
35 |   trace                 : Maybe Trace
36 |   workspaceFolders      : Maybe (OneOf [List WorkspaceFolder, Null])
37 |   workDoneToken         : Maybe ProgressToken
38 | %runElab deriveJSON defaultOpts `{InitializeParams}
39 |
40 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
41 | public export
42 | record InitializeResult where
43 |   constructor MkInitializeResult
44 |   capabilities : ServerCapabilities
45 |   serverInfo   : Maybe ServerInfo
46 | %runElab deriveJSON defaultOpts `{InitializeResult}
47 |
48 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
49 | public export
50 | record InitializeError where
51 |   constructor MkInitializeError
52 |   retry : Bool
53 | %runElab deriveJSON defaultOpts `{InitializeError}
54 |
55 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialized
56 | public export
57 | record InitializedParams where
58 |   constructor MkInitializedParams
59 | %runElab deriveJSON defaultOpts `{InitializedParams}
60 |