0 | module Language.LSP.Message.DocumentFormatting
  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.TextDocument
  7 | import Language.LSP.Message.Utils
  8 | import Language.Reflection
  9 |
 10 | %language ElabReflection
 11 | %default total
 12 |
 13 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting
 14 | public export
 15 | record DocumentFormattingClientCapabilities where
 16 |   constructor MkDocumentFormattingClientCapabilities
 17 |   dynamicRegistration : Maybe Bool
 18 | %runElab deriveJSON defaultOpts `{DocumentFormattingClientCapabilities}
 19 |
 20 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting
 21 | public export
 22 | record DocumentFormattingOptions where
 23 |   constructor MkDocumentFormattingOptions
 24 |   workDoneProgress : Maybe Bool
 25 | %runElab deriveJSON defaultOpts `{DocumentFormattingOptions}
 26 |
 27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting
 28 | public export
 29 | record DocumentFormattingRegistrationOptions where
 30 |   constructor MkDocumentFormattingRegistrationOptions
 31 |   workDoneProgress : Maybe Bool
 32 |   documentSelector : OneOf [DocumentSelector, Null]
 33 | %runElab deriveJSON defaultOpts `{DocumentFormattingRegistrationOptions}
 34 |
 35 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting
 36 | public export
 37 | record FormattingOptions where
 38 |   constructor MkFormattingOptions
 39 |   tabSize                : Int
 40 |   insertSpaces           : Bool
 41 |   trimTrailingWhitespace : Maybe Bool
 42 |   insertFinalNewline     : Maybe Bool
 43 |   trimFinalNewlines      : Maybe Bool
 44 |   other                  : List (String, OneOf [Bool, Int, String])
 45 |
 46 | export
 47 | ToJSON FormattingOptions where
 48 |   toJSON opts =
 49 |     JObject ((catMaybes [ Just ("tabSize", toJSON opts.tabSize)
 50 |                         , Just ("insertSpaces", toJSON opts.insertSpaces)
 51 |                         , ("trimTrailingWhitespace",) . toJSON <$> opts.trimTrailingWhitespace
 52 |                         , ("insertFinalNewline",) . toJSON <$> opts.insertFinalNewline
 53 |                         , ("trimFinalNewlines",) . toJSON <$> opts.trimFinalNewlines
 54 |                         ]) ++ (mapSnd toJSON <$> opts.other))
 55 |
 56 | export
 57 | FromJSON FormattingOptions where
 58 |   fromJSON (JObject arg) =
 59 |       pure MkFormattingOptions <*> (lookup "tabSize" arg >>= fromJSON)
 60 |                                <*> (lookup "insertSpaces" arg >>= fromJSON)
 61 |                                <*> (pure $ lookup "trimTrailingWhitespace" arg >>= fromJSON)
 62 |                                <*> (pure $ lookup "insertFinalNewline" arg >>= fromJSON)
 63 |                                <*> (pure $ lookup "trimFinalNewlines" arg >>= fromJSON)
 64 |                                <*> (pure $ catMaybes $ map sequence $ map (mapSnd fromJSON) $ filter (\(k, _) => not $ k `elem` fields) $ toList arg)
 65 |     where
 66 |       fields : List String
 67 |       fields = ["tabSize", "insertSpaces", "trimTrailingWhitespace", "insertFinalNewline", "trimFinalNewlines"]
 68 |   fromJSON _ = neutral
 69 |
 70 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting
 71 | public export
 72 | record DocumentFormattingParams where
 73 |   constructor MkDocumentFormattingParams
 74 |   workDoneToken : Maybe ProgressToken
 75 |   textDocument  : TextDocumentIdentifier
 76 |   options       : FormattingOptions
 77 | %runElab deriveJSON defaultOpts `{DocumentFormattingParams}
 78 |
 79 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting
 80 | public export
 81 | record DocumentRangeFormattingClientCapabilities where
 82 |   constructor MkDocumentRangeFormattingClientCapabilities
 83 |   dynamicRegistration : Maybe Bool
 84 | %runElab deriveJSON defaultOpts `{DocumentRangeFormattingClientCapabilities}
 85 |
 86 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting
 87 | public export
 88 | record DocumentRangeFormattingOptions where
 89 |   constructor MkDocumentRangeFormattingOptions
 90 |   workDoneProgress : Maybe Bool
 91 | %runElab deriveJSON defaultOpts `{DocumentRangeFormattingOptions}
 92 |
 93 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting
 94 | public export
 95 | record DocumentRangeFormattingRegistrationOptions where
 96 |   constructor MkDocumentRangeFormattingRegistrationOptions
 97 |   workDoneProgress : Maybe Bool
 98 |   documentSelector : OneOf [DocumentSelector, Null]
 99 | %runElab deriveJSON defaultOpts `{DocumentRangeFormattingRegistrationOptions}
100 |
101 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting
102 | public export
103 | record DocumentRangeFormattingParams where
104 |   constructor MkDocumentRangeFormattingParams
105 |   workDoneToken : Maybe ProgressToken
106 |   textDocument  : TextDocumentIdentifier
107 |   range         : Range
108 |   options       : FormattingOptions
109 | %runElab deriveJSON defaultOpts `{DocumentRangeFormattingParams}
110 |
111 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting
112 | public export
113 | record DocumentOnTypeFormattingClientCapabilities where
114 |   constructor MkDocumentOnTypeFormattingClientCapabilities
115 |   dynamicRegistration : Maybe Bool
116 | %runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingClientCapabilities}
117 |
118 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting
119 | public export
120 | record DocumentOnTypeFormattingOptions where
121 |   constructor MkDocumentOnTypeFormattingOptions
122 |   firstTriggerCharacter : Char
123 |   moreTriggerCharacter  : Maybe (List Char)
124 | %runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingOptions}
125 |
126 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting
127 | public export
128 | record DocumentOnTypeFormattingRegistrationOptions where
129 |   constructor MkDocumentOnTypeFormattingRegistrationOptions
130 |   firstTriggerCharacter : Char
131 |   moreTriggerCharacter  : Maybe (List Char)
132 |   documentSelector      : OneOf [DocumentSelector, Null]
133 | %runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingRegistrationOptions}
134 |
135 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting
136 | public export
137 | record DocumentOnTypeFormattingParams where
138 |   constructor MkDocumentOnTypeFormattingParams
139 |   textDocument : TextDocumentIdentifier
140 |   ch           : Char
141 |   options      : FormattingOptions
142 | %runElab deriveJSON defaultOpts `{DocumentOnTypeFormattingParams}
143 |