0 | module Language.LSP.Message.Window
  1 |
  2 | import Language.JSON
  3 | import Language.LSP.Message.Derive
  4 | import Language.LSP.Message.Location
  5 | import Language.LSP.Message.Progress
  6 | import Language.LSP.Message.URI
  7 | import Language.LSP.Message.Utils
  8 | import Language.Reflection
  9 |
 10 | %language ElabReflection
 11 | %default total
 12 |
 13 | namespace MessageType
 14 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
 15 |   public export
 16 |   data MessageType = Error | Warning | Info | Log
 17 |
 18 | export
 19 | ToJSON MessageType where
 20 |   toJSON Error   = JNumber 1
 21 |   toJSON Warning = JNumber 2
 22 |   toJSON Info    = JNumber 3
 23 |   toJSON Log     = JNumber 4
 24 |
 25 | export
 26 | FromJSON MessageType where
 27 |   fromJSON (JNumber 1) = pure Error
 28 |   fromJSON (JNumber 2) = pure Warning
 29 |   fromJSON (JNumber 3) = pure Info
 30 |   fromJSON (JNumber 4) = pure Log
 31 |   fromJSON _ = Nothing
 32 |
 33 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
 34 | public export
 35 | record ShowMessageParams where
 36 |   constructor MkShowMessageParams
 37 |   type    : MessageType
 38 |   message : String
 39 | %runElab deriveJSON defaultOpts `{ShowMessageParams}
 40 |
 41 | namespace ShowMessageRequestClientCapabilities
 42 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
 43 |   public export
 44 |   record ShowMessageActionItem where
 45 |     constructor MkShowMessageActionItem
 46 |     additionalPropertiesSupport : Maybe Bool
 47 |   %runElab deriveJSON defaultOpts `{ShowMessageActionItem}
 48 |
 49 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
 50 | public export
 51 | record ShowMessageRequestClientCapabilities where
 52 |   constructor MkShowMessageRequestClientCapabilities
 53 |   messageActionItem : Maybe ShowMessageActionItem
 54 | %runElab deriveJSON defaultOpts `{ShowMessageRequestClientCapabilities}
 55 |
 56 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
 57 | public export
 58 | record MessageActionItem where
 59 |   constructor MkMessageActionItem
 60 |   title : String
 61 | %runElab deriveJSON defaultOpts `{MessageActionItem}
 62 |
 63 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
 64 | public export
 65 | record ShowMessageRequestParams where
 66 |   constructor MkShowMessageRequestParams
 67 |   type    : MessageType
 68 |   message : String
 69 |   actions : Maybe (List MessageActionItem)
 70 | %runElab deriveJSON defaultOpts `{ShowMessageRequestParams}
 71 |
 72 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument
 73 | public export
 74 | record ShowDocumentClientCapabilities where
 75 |   constructor MkShowDocumentClientCapabilities
 76 |   support : Bool
 77 | %runElab deriveJSON defaultOpts `{ShowDocumentClientCapabilities}
 78 |
 79 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument
 80 | public export
 81 | record ShowDocumentParams where
 82 |   constructor MkShowDocumentParams
 83 |   uri       : URI
 84 |   external_ : Maybe Bool
 85 |   takeFocus : Maybe Bool
 86 |   selection : Maybe Range
 87 | %runElab deriveJSON ({renames := [("external_", "external")]} defaultOpts) `{ShowDocumentParams}
 88 |
 89 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument
 90 | public export
 91 | record ShowDocumentResult where
 92 |   constructor MkShowDocumentResult
 93 |   success : Bool
 94 | %runElab deriveJSON defaultOpts `{ShowDocumentResult}
 95 |
 96 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_logMessage
 97 | public export
 98 | record LogMessageParams where
 99 |   constructor MkLogMessageParams
100 |   type    : MessageType
101 |   message : String
102 | %runElab deriveJSON defaultOpts `{LogMessageParams}
103 |
104 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_create
105 | public export
106 | record WorkDoneProgressCreateParams where
107 |   constructor MkWorkDoneProgressCreateParams
108 |   token : ProgressToken
109 | %runElab deriveJSON defaultOpts `{WorkDoneProgressCreateParams}
110 |
111 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_cancel
112 | public export
113 | record WorkDoneProgressCancelParams where
114 |   constructor MkWorkDoneProgressCancelParams
115 |   token : ProgressToken
116 | %runElab deriveJSON defaultOpts `{WorkDoneProgressCancelParams}
117 |