0 | module Language.LSP.Message.Markup
 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 | namespace MarkupKind
11 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent
12 |   public export
13 |   data MarkupKind = PlainText | Markdown
14 |
15 | public export
16 | Eq MarkupKind where
17 |   PlainText == PlainText = True
18 |   PlainText == _ = False
19 |   Markdown == Markdown = True
20 |   Markdown == _ = False
21 |
22 | export
23 | ToJSON MarkupKind where
24 |   toJSON PlainText = JString "plaintext"
25 |   toJSON Markdown  = JString "markdown"
26 |
27 | export
28 | FromJSON MarkupKind where
29 |   fromJSON (JString "plaintext") = pure PlainText
30 |   fromJSON (JString "markdown")  = pure Markdown
31 |   fromJSON _ = neutral
32 |
33 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent
34 | public export
35 | record MarkupContent where
36 |   constructor MkMarkupContent
37 |   kind : MarkupKind
38 |   value : String
39 | %runElab deriveJSON defaultOpts `{MarkupContent}
40 |
41 | namespace MarkedString
42 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
43 |   public export
44 |   record MarkedStringWithLanguage where
45 |     constructor MkMarkedStringWithLanguage
46 |     language : String
47 |     value : String
48 |   %runElab deriveJSON defaultOpts `{MarkedStringWithLanguage}
49 |
50 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
51 | public export
52 | MarkedString : Type
53 | MarkedString = OneOf [String, MarkedStringWithLanguage]
54 |
55 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent
56 | public export
57 | record MarkdownClientCapabilities where
58 |   constructor MkMarkdownClientCapabilities
59 |   parser  : String
60 |   version : Maybe String
61 | %runElab deriveJSON defaultOpts `{MarkdownClientCapabilities}
62 |