Documentation

Lean.Server.Requests

structure Lean.Server.RequestError :

Type

code : Lean.JsonRpc.ErrorCode
message : String

def Lean.Server.RequestError.fileChanged :

Lean.Server.RequestError

Equations

Lean.Server.RequestError.fileChanged = { code := Lean.JsonRpc.ErrorCode.contentModified, message := "File changed." }

def Lean.Server.RequestError.methodNotFound (method : String) :

Lean.Server.RequestError

Equations

Lean.Server.RequestError.methodNotFound method = { code := Lean.JsonRpc.ErrorCode.methodNotFound, message := toString "No request handler found for '" ++ toString method ++ toString "'" }

instance Lean.Server.RequestError.instCoeErrorRequestError :

Coe IO.Error Lean.Server.RequestError

Equations

Lean.Server.RequestError.instCoeErrorRequestError = { coe := fun e => { code := Lean.JsonRpc.ErrorCode.internalError, message := toString e } }

def Lean.Server.RequestError.toLspResponseError (id : Lean.JsonRpc.RequestID) (e : Lean.Server.RequestError) :

Lean.JsonRpc.ResponseError Unit

Equations

Lean.Server.RequestError.toLspResponseError id e = { id := id, code := e.code, message := e.message, data? := none }

def Lean.Server.parseRequestParams (paramType : Type) [inst : Lean.FromJson paramType] (params : Lean.Json) :

Except Lean.Server.RequestError paramType

Equations

Lean.Server.parseRequestParams paramType params = Except.mapError (fun inner => { code := Lean.JsonRpc.ErrorCode.parseError, message := toString "Cannot parse request params: " ++ toString (Lean.Json.compress params) ++ toString "\n" ++ toString inner ++ toString "" }) (Lean.fromJson? params)

structure Lean.Server.RequestContext :

Type

rpcSessions : Std.RBMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare
srcSearchPath : Lean.SearchPath
doc : Lean.Server.FileWorker.EditableDocument
hLog : IO.FS.Stream
initParams : Lean.Lsp.InitializeParams

@[inline]

abbrev Lean.Server.RequestTask (α : Type u_1) :

Type u_1

Equations

Lean.Server.RequestTask α = Task (Except Lean.Server.RequestError α)

@[inline]

abbrev Lean.Server.RequestM (α : Type) :

Type

Equations

Lean.Server.RequestM = ReaderT Lean.Server.RequestContext (EIO Lean.Server.RequestError)

instance Lean.Server.instInhabitedRequestM {α : Type} :

Inhabited (Lean.Server.RequestM α)

Equations

Lean.Server.instInhabitedRequestM = { default := throw { code := Lean.JsonRpc.ErrorCode.internalError, message := toString (IO.userError "executing Inhabited instance?!") } }

instance Lean.Server.instMonadLiftIORequestM :

MonadLift IO Lean.Server.RequestM

Equations

Lean.Server.instMonadLiftIORequestM = { monadLift := fun {α} x => liftM (IO.toEIO (fun e => { code := Lean.JsonRpc.ErrorCode.internalError, message := toString e }) x) }

def Lean.Server.RequestM.readDoc :

Lean.Server.RequestM Lean.Server.FileWorker.EditableDocument

Equations

Lean.Server.RequestM.readDoc rc = pure rc.doc

def Lean.Server.RequestM.asTask {α : Type} (t : Lean.Server.RequestM α) :

Lean.Server.RequestM (Lean.Server.RequestTask α)

Equations

Lean.Server.RequestM.asTask t rc = do let t ← liftM (EIO.asTask (t rc) Task.Priority.default) pure (Task.map liftExcept t)

def Lean.Server.RequestM.mapTask {α : Type u_1} {β : Type} (t : Task α) (f : α → Lean.Server.RequestM β) :

Lean.Server.RequestM (Lean.Server.RequestTask β)

Equations

Lean.Server.RequestM.mapTask t f rc = do let t ← liftM (EIO.mapTask (fun a => f a rc) t Task.Priority.default) pure (Task.map liftExcept t)

def Lean.Server.RequestM.bindTask {α : Type u_1} {β : Type} (t : Task α) (f : α → Lean.Server.RequestM (Lean.Server.RequestTask β)) :

Lean.Server.RequestM (Lean.Server.RequestTask β)

Equations

Lean.Server.RequestM.bindTask t f rc = liftM (EIO.bindTask t (fun a => f a rc) Task.Priority.default)

def Lean.Server.RequestM.withWaitFindSnap {β : Type} (doc : Lean.Server.FileWorker.EditableDocument) (p : Lean.Server.Snapshots.Snapshot → Bool) (notFoundX : Lean.Server.RequestM β) (x : Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM β) :

Lean.Server.RequestM (Lean.Server.RequestTask β)

Equations

Lean.Server.RequestM.withWaitFindSnap doc p notFoundX x = do let findTask ← liftM (IO.AsyncList.waitFind? p (Lean.Server.FileWorker.EditableDocument.allSnaps doc)) Lean.Server.RequestM.mapTask findTask fun x => match x with | Except.error Lean.Server.FileWorker.ElabTaskError.aborted => throwThe Lean.Server.RequestError Lean.Server.RequestError.fileChanged | Except.error (Lean.Server.FileWorker.ElabTaskError.ioError e) => throw { code := Lean.JsonRpc.ErrorCode.internalError, message := toString e } | Except.ok none => notFoundX | Except.ok (some snap) => x snap

structure Lean.Server.RequestHandler :

Type

fileSource : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri
handle : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)

constant Lean.Server.requestHandlers :

IO.Ref (Std.PersistentHashMap String Lean.Server.RequestHandler)

def Lean.Server.registerLspRequestHandler (method : String) (paramType : Type) [inst : Lean.FromJson paramType] [inst : Lean.Lsp.FileSource paramType] (respType : Type) [inst : Lean.ToJson respType] (handler : paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) :

Equations

Lean.Server.registerLspRequestHandler method paramType respType handler = do let a ← liftM IO.initializing let _do_jp : PUnit → IO Unit := fun y => do let a ← ST.Ref.get Lean.Server.requestHandlers let _do_jp : PUnit → IO Unit := fun y => let fileSource := fun j => Except.map Lean.Lsp.fileSource (Lean.Server.parseRequestParams paramType j); let handle := fun j => do let params ← liftExcept (Lean.Server.parseRequestParams paramType j) let t ← handler params pure (Task.map (Except.map Lean.toJson) t); ST.Ref.modify Lean.Server.requestHandlers fun rhs => Std.PersistentHashMap.insert rhs method { fileSource := fileSource, handle := handle } if Std.PersistentHashMap.contains a method = true then do let y ← throw (IO.userError (toString "Failed to register LSP request handler for '" ++ toString method ++ toString "': already registered")) _do_jp y else do let y ← pure PUnit.unit _do_jp y if (!a) = true then do let y ← throw (IO.userError (toString "Failed to register LSP request handler for '" ++ toString method ++ toString "': only possible during initialization")) _do_jp y else do let y ← pure PUnit.unit _do_jp y

def Lean.Server.lookupLspRequestHandler (method : String) :

IO (Option Lean.Server.RequestHandler)

Equations

Lean.Server.lookupLspRequestHandler method = do let a ← ST.Ref.get Lean.Server.requestHandlers pure (Std.PersistentHashMap.find? a method)

def Lean.Server.chainLspRequestHandler (method : String) (paramType : Type) [inst : Lean.FromJson paramType] (respType : Type) [inst : Lean.FromJson respType] [inst : Lean.ToJson respType] (handler : paramType → Lean.Server.RequestTask respType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) :

Equations

Lean.Server.chainLspRequestHandler method paramType respType handler = do let a ← liftM IO.initializing let _do_jp : PUnit → IO Unit := fun y => do let a ← Lean.Server.lookupLspRequestHandler method match a with | some oldHandler => let handle := fun j => do let t ← Lean.Server.RequestHandler.handle oldHandler j let t ← pure (Task.map (fun x => Except.bind x fun j => Except.mapError (fun e => { code := Lean.JsonRpc.ErrorCode.internalError, message := toString (IO.userError (toString "Failed to parse original LSP response for `" ++ toString method ++ toString "` when chaining: " ++ toString e ++ toString "")) }) (Lean.fromJson? j)) t) let params ← liftExcept (Lean.Server.parseRequestParams paramType j) let t ← handler params t pure (Task.map (Except.map Lean.toJson) t); ST.Ref.modify Lean.Server.requestHandlers fun rhs => Std.PersistentHashMap.insert rhs method { fileSource := oldHandler.fileSource, handle := handle } | x => throw (IO.userError (toString "Failed to chain LSP request handler for '" ++ toString method ++ toString "': no initial handler registered")) if (!a) = true then do let y ← throw (IO.userError (toString "Failed to chain LSP request handler for '" ++ toString method ++ toString "': only possible during initialization")) _do_jp y else do let y ← pure PUnit.unit _do_jp y

def Lean.Server.routeLspRequest (method : String) (params : Lean.Json) :

IO (Except Lean.Server.RequestError Lean.Lsp.DocumentUri)

Equations

Lean.Server.routeLspRequest method params = do let a ← Lean.Server.lookupLspRequestHandler method match a with | none => pure (Except.error (Lean.Server.RequestError.methodNotFound method)) | some rh => pure (Lean.Server.RequestHandler.fileSource rh params)

def Lean.Server.handleLspRequest (method : String) (params : Lean.Json) :

Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)

Equations

Lean.Server.handleLspRequest method params = do let a ← liftM (Lean.Server.lookupLspRequestHandler method) match a with | none => throw { code := Lean.JsonRpc.ErrorCode.internalError, message := toString (IO.userError (toString "internal server error: request '" ++ toString method ++ toString "' routed through watchdog but unknown in worker; are both using the same plugins?")) } | some rh => Lean.Server.RequestHandler.handle rh params