
  0 | module Language.LSP.Message.Trace
  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 Trace
 11 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#traceValue
 12 |   public export
 13 |   data Trace = TraceOff | TraceMessages | TraceVerbose
 14 | 
 15 | export
 16 | ToJSON Trace where
 17 |   toJSON TraceOff      = JString "off"
 18 |   toJSON TraceMessages = JString "messages"
 19 |   toJSON TraceVerbose  = JString "verbose"
 20 | 
 21 | export
 22 | FromJSON Trace where
 23 |   fromJSON (JString "off")      = pure TraceOff
 24 |   fromJSON (JString "messages") = pure TraceMessages
 25 |   fromJSON (JString "verbose")  = pure TraceVerbose
 26 |   fromJSON _ = neutral
 27 | 
 28 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#setTrace
 29 | public export
 30 | record SetTraceParams where
 31 |   constructor MkSetTraceParams
 32 |   value : Trace
 33 | %runElab deriveJSON defaultOpts `{SetTraceParams}
 34 | 
 35 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#logTrace
 36 | public export
 37 | record LogTraceParams where
 38 |   constructor MkLogTraceParams
 39 |   message : String
 40 |   verbose : Maybe String
 41 | %runElab deriveJSON defaultOpts `{LogTraceParams}
 42 |