0 | module Language.LSP.Message.Markup

 2 | import Language.JSON

 3 | import Language.LSP.Message.Derive

 4 | import Language.LSP.Message.Utils

 5 | import Language.Reflection

 7 | %language ElabReflection

 8 | %default total

10 | namespace MarkupKind

11 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent

12 |   public export

13 |   data MarkupKind = PlainText | Markdown

15 | public export

16 | Eq MarkupKind where

17 |   PlainText == PlainText = True

18 |   PlainText == _ = False

19 |   Markdown == Markdown = True

20 |   Markdown == _ = False

23 | ToJSON MarkupKind where

24 |   toJSON PlainText = JString "plaintext"

25 |   toJSON Markdown  = JString "markdown"

28 | FromJSON MarkupKind where

29 |   fromJSON (JString "plaintext") = pure PlainText

30 |   fromJSON (JString "markdown")  = pure Markdown

31 |   fromJSON _ = neutral

34 | public export

35 | record MarkupContent where

36 |   constructor MkMarkupContent

37 |   kind : MarkupKind

38 |   value : String

39 | %runElab deriveJSON defaultOpts `{MarkupContent}

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}

51 | public export

52 | MarkedString : Type

53 | MarkedString = OneOf [String, MarkedStringWithLanguage]

56 | public export

57 | record MarkdownClientCapabilities where

58 |   constructor MkMarkdownClientCapabilities

59 |   parser  : String

60 |   version : Maybe String

61 | %runElab deriveJSON defaultOpts `{MarkdownClientCapabilities}