structure Lean.Server.Logging.LogConfig : Type

• isEnabled : Bool
• logFile : System.FilePath
• allowedMethods? : Option (Std.HashSet String)
• disallowedMethods? : Option (Std.HashSet String)

def Lean.Server.Logging.LogConfig.ofLspLogConfig (lspCfg? : Option Lsp.LogConfig) : IO LogConfig

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.Server.Logging.MessageMethod : Type

• request (method : String) : MessageMethod
• rpcRequest (method : String) : MessageMethod
• notification (method : String) : MessageMethod

def Lean.Server.Logging.instInhabitedMessageMethod.default : MessageMethod

Equations

• Lean.Server.Logging.instInhabitedMessageMethod.default = Lean.Server.Logging.MessageMethod.request default

instance Lean.Server.Logging.instInhabitedMessageMethod : Inhabited MessageMethod

Equations

• Lean.Server.Logging.instInhabitedMessageMethod = { default := Lean.Server.Logging.instInhabitedMessageMethod.default }

def Lean.Server.Logging.messageMethod? : JsonRpc.Message → Option MessageMethod

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.Logging.messageMethod? (Lean.JsonRpc.Message.notification method params?) = some (Lean.Server.Logging.MessageMethod.notification method)
• Lean.Server.Logging.messageMethod? x✝ = none

def Lean.Server.Logging.writeLogEntry (cfg : LogConfig) (pending : Std.HashMap JsonRpc.RequestID MessageMethod) (log : IO.FS.Handle) (direction : JsonRpc.MessageDirection) (msg : JsonRpc.Message) : IO Unit

Equations

• One or more equations did not get rendered due to their size.