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

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

instance Lean.Server.Logging.instInhabitedMessageMethod : Inhabited MessageMethod

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

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