0 | module Language.LSP.Message.Progress
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Derive
 4 | import Language.LSP.Message.Utils
 5 | import Language.Reflection
 6 |
 7 | %language ElabReflection
 8 | %default total
 9 |
10 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#progress
11 | public export
12 | ProgressToken : Type
13 | ProgressToken = OneOf [Int, String]
14 |
15 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#clientInitiatedProgress
16 | public export
17 | record WorkDoneProgressOptions where
18 |   constructor MkWorkDoneProgressOptions
19 |   workDoneProgress : Maybe Bool
20 | %runElab deriveJSON defaultOpts `{WorkDoneProgressOptions}
21 |
22 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#clientInitiatedProgress
23 | public export
24 | record WorkDoneProgressParams where
25 |   constructor MkWorkDoneProgressParams
26 |   workDoneToken : Maybe ProgressToken
27 | %runElab deriveJSON defaultOpts `{WorkDoneProgressParams}
28 |
29 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#partialResultParams
30 | public export
31 | record PartialResultParams where
32 |   constructor MkPartialResultParams
33 |   partialResultToken : Maybe ProgressToken
34 | %runElab deriveJSON defaultOpts `{PartialResultParams}
35 |
36 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressBegin
37 | public export
38 | record WorkDoneProgressBegin where
39 |   constructor MkWorkDoneProgressBegin
40 |   title : String
41 |   cancellable : Maybe Bool
42 |   message : Maybe String
43 |   percentage : Maybe Int
44 | %runElab deriveJSON ({staticFields := [("kind", JString "begin")]} defaultOpts) `{WorkDoneProgressBegin}
45 |
46 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressReport
47 | public export
48 | record WorkDoneProgressReport where
49 |   constructor MkWorkDoneProgressReport
50 |   cancellable : Maybe Bool
51 |   message : Maybe String
52 |   percentage : Maybe Int
53 | %runElab deriveJSON ({staticFields := [("kind", JString "report")]} defaultOpts) `{WorkDoneProgressReport}
54 |
55 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressEnd
56 | public export
57 | record WorkDoneProgressEnd where
58 |   constructor MkWorkDoneProgressEnd
59 |   message : Maybe String
60 | %runElab deriveJSON ({staticFields := [("kind", JString "end")]} defaultOpts) `{WorkDoneProgressEnd}
61 |