0 | module Language.LSP.Message.Location
 1 |
 2 | import Data.URI
 3 | import Language.JSON
 4 | import Language.LSP.Message.Derive
 5 | import Language.LSP.Message.URI
 6 | import Language.LSP.Message.Utils
 7 | import Language.Reflection
 8 |
 9 | %hide Prelude.Range
10 | %language ElabReflection
11 | %default total
12 |
13 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#position
14 | public export
15 | record Position where
16 |   constructor MkPosition
17 |   line      : Int
18 |   character : Int
19 | %runElab deriveJSON defaultOpts `{Position}
20 |
21 | export
22 | Eq Position where
23 |   (MkPosition line1 char1) == (MkPosition line2 char2) = line1 == line2 && char1 == char2
24 |
25 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#range
26 | public export
27 | record Range where
28 |   constructor MkRange
29 |   start : Position
30 |   end   : Position
31 | %runElab deriveJSON defaultOpts `{Range}
32 |
33 | export
34 | Eq Range where
35 |   (MkRange start1 end1) == (MkRange start2 end2) = start1 == start2 && end1 == end2
36 |
37 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#location
38 | public export
39 | record Location where
40 |   constructor MkLocation
41 |   uri   : URI
42 |   range : Range
43 | %runElab deriveJSON defaultOpts `{Location}
44 |
45 | export
46 | Eq Location where
47 |   (MkLocation uri1 range1) == (MkLocation uri2 range2) = uri1 == uri2 && range1 == range2
48 |
49 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#locationLink
50 | public export
51 | record LocationLink where
52 |   constructor MkLocationLink
53 |   originSelectionRange : Maybe Range
54 |   targetUri            : URI
55 |   targetRange          : Range
56 |   targetSelectionRange : Range
57 | %runElab deriveJSON defaultOpts `{LocationLink}
58 |