Request Context

structure Lapis.Concurrent.LspActor.RequestContext (UserState : Type) : Type

Context passed to request handlers

• vfs : VfsActor.VfsRef

  VFS reference for document access

• outputChannel : Transport.OutputChannel

  Output channel for sending messages

• pendingResponses : Server.Receiver.PendingResponses

  Pending responses for server-initiated requests

• userStateRef : IO.Ref UserState

  Mutable user state reference

• capabilities : Protocol.Capabilities.ServerCapabilities

  Server capabilities

• serverInfo : Protocol.Messages.ServerInfo

  Server info

• progressManager : Server.Progress.ProgressManager

  Progress manager for work done progress

• cancelToken : IO.CancelToken

  Cancellation token for this request

def Lapis.Concurrent.LspActor.RequestContext.isCancelled {UserState : Type} (ctx : RequestContext UserState) : IO Bool

Check if request was cancelled

Equations

• ctx.isCancelled = liftM ctx.cancelToken.isSet

def Lapis.Concurrent.LspActor.RequestContext.getUserState {UserState : Type} (ctx : RequestContext UserState) : IO UserState

Get user state

Equations

• ctx.getUserState = ST.Ref.get ctx.userStateRef

def Lapis.Concurrent.LspActor.RequestContext.setUserState {UserState : Type} (ctx : RequestContext UserState) (state : UserState) : IO Unit

Set user state

Equations

• ctx.setUserState state = ST.Ref.set ctx.userStateRef state

def Lapis.Concurrent.LspActor.RequestContext.modifyUserState {UserState : Type} (ctx : RequestContext UserState) (f : UserState → UserState) : IO Unit

Modify user state

Equations

• ctx.modifyUserState f = ST.Ref.modify ctx.userStateRef f

def Lapis.Concurrent.LspActor.RequestContext.getDocument {UserState : Type} (ctx : RequestContext UserState) (uri : Protocol.Types.DocumentUri) : IO (Option VfsActor.DocumentSnapshot)

Get a document snapshot

Equations

• ctx.getDocument uri = ctx.vfs.getSnapshot uri

def Lapis.Concurrent.LspActor.RequestContext.getDocumentContent {UserState : Type} (ctx : RequestContext UserState) (uri : Protocol.Types.DocumentUri) : IO (Option String)

Get document content

Equations

• ctx.getDocumentContent uri = ctx.vfs.getContent uri

def Lapis.Concurrent.LspActor.RequestContext.getDocumentLine {UserState : Type} (ctx : RequestContext UserState) (uri : Protocol.Types.DocumentUri) (line : Nat) : IO (Option String)

Get a line from a document

Equations

• ctx.getDocumentLine uri line = ctx.vfs.getLine uri line

def Lapis.Concurrent.LspActor.RequestContext.getWordAt {UserState : Type} (ctx : RequestContext UserState) (uri : Protocol.Types.DocumentUri) (pos : Protocol.Types.Position) : IO (Option String)

Get word at position

Equations

• ctx.getWordAt uri pos = ctx.vfs.getWordAt uri pos

def Lapis.Concurrent.LspActor.RequestContext.sendNotification {UserState : Type} (ctx : RequestContext UserState) (method : String) (params : Lean.Json) : IO Unit

Send a notification to the client

Equations

• ctx.sendNotification method params = ctx.outputChannel.send (Lapis.Protocol.JsonRpc.Message.notification { method := method, params := some params })

def Lapis.Concurrent.LspActor.RequestContext.sendRequest {UserState : Type} (ctx : RequestContext UserState) (method : String) (params : Lean.Json) : IO (IO.Promise Lean.Json)

Send a request to the client

Equations

• ctx.sendRequest method params = do let promise ← liftM IO.Promise.new let requestId ← ctx.pendingResponses.register promise ctx.outputChannel.sendRequest requestId method params pure promise

def Lapis.Concurrent.LspActor.RequestContext.publishDiagnostics {UserState : Type} (ctx : RequestContext UserState) (params : Protocol.Messages.PublishDiagnosticsParams) : IO Unit

Publish diagnostics

Equations

• ctx.publishDiagnostics params = ctx.sendNotification "textDocument/publishDiagnostics" (Lean.toJson params)

def Lapis.Concurrent.LspActor.RequestContext.logMessage {UserState : Type} (ctx : RequestContext UserState) (type : Nat) (message : String) : IO Unit

Log a message

Equations

• ctx.logMessage type message = ctx.sendNotification "window/logMessage" (Lean.Json.mkObj [("type", Lean.Json.num (Lean.JsonNumber.fromNat type)), ("message", Lean.Json.str message)])

def Lapis.Concurrent.LspActor.RequestContext.logInfo {UserState : Type} (ctx : RequestContext UserState) (message : String) : IO Unit

Log info

Equations

• ctx.logInfo message = ctx.logMessage 3 message

def Lapis.Concurrent.LspActor.RequestContext.logWarning {UserState : Type} (ctx : RequestContext UserState) (message : String) : IO Unit

Log warning

Equations

• ctx.logWarning message = ctx.logMessage 2 message

def Lapis.Concurrent.LspActor.RequestContext.logError {UserState : Type} (ctx : RequestContext UserState) (message : String) : IO Unit

Log error

Equations

• ctx.logError message = ctx.logMessage 1 message

def Lapis.Concurrent.LspActor.RequestContext.showMessage {UserState : Type} (ctx : RequestContext UserState) (type : Nat) (message : String) : IO Unit

Show a message to the user

Equations

• ctx.showMessage type message = ctx.sendNotification "window/showMessage" (Lean.Json.mkObj [("type", Lean.Json.num (Lean.JsonNumber.fromNat type)), ("message", Lean.Json.str message)])

def Lapis.Concurrent.LspActor.RequestContext.showInfo {UserState : Type} (ctx : RequestContext UserState) (message : String) : IO Unit

Show info message

Equations

• ctx.showInfo message = ctx.showMessage 3 message

def Lapis.Concurrent.LspActor.RequestContext.showWarning {UserState : Type} (ctx : RequestContext UserState) (message : String) : IO Unit

Show warning message

Equations

• ctx.showWarning message = ctx.showMessage 2 message

def Lapis.Concurrent.LspActor.RequestContext.showError {UserState : Type} (ctx : RequestContext UserState) (message : String) : IO Unit

Show error message

Equations

• ctx.showError message = ctx.showMessage 1 message

def Lapis.Concurrent.LspActor.RequestContext.withProgress {UserState α : Type} (ctx : RequestContext UserState) (title : String) (cancellable : Bool := false) (action : Server.Progress.ProgressHandle → IO α) : IO α

Run an action with progress reporting

Equations

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

Handler Types

inductive Lapis.Concurrent.LspActor.HandlerResult : Type

Result of handling a request

• ok (result : Lean.Json) : HandlerResult
• error (code : Int) (message : String) : HandlerResult

def Lapis.Concurrent.LspActor.instInhabitedHandlerResult.default : HandlerResult

Equations

• Lapis.Concurrent.LspActor.instInhabitedHandlerResult.default = Lapis.Concurrent.LspActor.HandlerResult.ok default

instance Lapis.Concurrent.LspActor.instInhabitedHandlerResult : Inhabited HandlerResult

Equations

• Lapis.Concurrent.LspActor.instInhabitedHandlerResult = { default := Lapis.Concurrent.LspActor.instInhabitedHandlerResult.default }

def Lapis.Concurrent.LspActor.RequestHandler (UserState : Type) : Type

A request handler in the actor model

Equations

• Lapis.Concurrent.LspActor.RequestHandler UserState = (Lapis.Concurrent.LspActor.RequestContext UserState → Lean.Json → IO Lapis.Concurrent.LspActor.HandlerResult)

def Lapis.Concurrent.LspActor.NotificationHandler (UserState : Type) : Type

A notification handler in the actor model

Equations

• Lapis.Concurrent.LspActor.NotificationHandler UserState = (Lapis.Concurrent.LspActor.RequestContext UserState → Lean.Json → IO Unit)

LSP Messages

inductive Lapis.Concurrent.LspActor.LspMsg (UserState : Type) : Type

Messages for the LSP actor

• request {UserState : Type} (msg : Protocol.JsonRpc.RequestMessage) : LspMsg UserState

  Handle an incoming request

• notification {UserState : Type} (msg : Protocol.JsonRpc.NotificationMessage) : LspMsg UserState

  Handle an incoming notification (non-document)

• cancelRequest {UserState : Type} (id : Protocol.JsonRpc.RequestId) : LspMsg UserState

  Cancel a pending request

• response {UserState : Type} (id : Protocol.JsonRpc.RequestId) (result : Lean.Json) : LspMsg UserState

  Handle a response from the client

• errorResponse {UserState : Type} (id : Protocol.JsonRpc.RequestId) (error : String) : LspMsg UserState

  Handle an error response from the client

• shutdown {UserState : Type} : LspMsg UserState

  Shutdown the actor

LSP Actor State

structure Lapis.Concurrent.LspActor.PendingRequest : Type

Pending request tracking

• id : Protocol.JsonRpc.RequestId
• cancelToken : IO.CancelToken
• task : Task (Except IO.Error Unit)

structure Lapis.Concurrent.LspActor.LspConfig (UserState : Type) : Type

LSP Actor configuration

• name : String

  Server name

• version : Option String

  Server version

• capabilities : Protocol.Capabilities.ServerCapabilities

  Server capabilities

• requestHandlers : Std.HashMap String (RequestHandler UserState)

  Request handlers by method

• notificationHandlers : Std.HashMap String (NotificationHandler UserState)

  Notification handlers by method

• maxConcurrentRequests : Nat

  Maximum concurrent requests

• initializeHook : Option (RequestContext UserState → Protocol.Messages.InitializeParams → IO Unit)

  Hook called on initialize

structure Lapis.Concurrent.LspActor.LspState (UserState : Type) : Type

LSP Actor state

• initialized : Bool

  Server initialized

• shutdownRequested : Bool

  Shutdown requested

• activeRequests : Nat

  Count of active requests (for backpressure)

LSP Actor Reference

structure Lapis.Concurrent.LspActor.LspRef (UserState : Type) : Type

Handle to the LSP actor

• ref : Actor.ActorRef (LspMsg UserState)

def Lapis.Concurrent.LspActor.LspRef.handleRequest {UserState : Type} (lsp : LspRef UserState) (msg : Protocol.JsonRpc.RequestMessage) : IO Unit

Send a request to be handled

Equations

• lsp.handleRequest msg = lsp.ref.send (Lapis.Concurrent.LspActor.LspMsg.request msg)

def Lapis.Concurrent.LspActor.LspRef.handleNotification {UserState : Type} (lsp : LspRef UserState) (msg : Protocol.JsonRpc.NotificationMessage) : IO Unit

Send a notification to be handled

Equations

• lsp.handleNotification msg = lsp.ref.send (Lapis.Concurrent.LspActor.LspMsg.notification msg)

def Lapis.Concurrent.LspActor.LspRef.cancelRequest {UserState : Type} (lsp : LspRef UserState) (id : Protocol.JsonRpc.RequestId) : IO Unit

Cancel a request

Equations

• lsp.cancelRequest id = lsp.ref.send (Lapis.Concurrent.LspActor.LspMsg.cancelRequest id)

def Lapis.Concurrent.LspActor.LspRef.handleResponse {UserState : Type} (lsp : LspRef UserState) (id : Protocol.JsonRpc.RequestId) (result : Lean.Json) : IO Unit

Handle a response from client

Equations

• lsp.handleResponse id result = lsp.ref.send (Lapis.Concurrent.LspActor.LspMsg.response id result)

def Lapis.Concurrent.LspActor.LspRef.handleErrorResponse {UserState : Type} (lsp : LspRef UserState) (id : Protocol.JsonRpc.RequestId) (error : String) : IO Unit

Handle an error response from client

Equations

• lsp.handleErrorResponse id error = lsp.ref.send (Lapis.Concurrent.LspActor.LspMsg.errorResponse id error)

def Lapis.Concurrent.LspActor.LspRef.shutdown {UserState : Type} (lsp : LspRef UserState) : IO Unit

Shutdown the actor

Equations

• lsp.shutdown = lsp.ref.send Lapis.Concurrent.LspActor.LspMsg.shutdown

LSP Actor Context

structure Lapis.Concurrent.LspActor.LspRuntime (UserState : Type) : Type

Runtime context for the LSP actor

• config : LspConfig UserState
• vfs : VfsActor.VfsRef
• outputChannel : Transport.OutputChannel
• pendingResponses : Server.Receiver.PendingResponses
• userStateRef : IO.Ref UserState
• progressManager : Server.Progress.ProgressManager

  Progress manager for work done progress

• pendingRequestsRef : IO.Ref (Std.HashMap String PendingRequest)

  Shared ref for pending requests (for async cleanup)

LSP Actor Implementation

Spawn LSP Actor

def Lapis.Concurrent.LspActor.spawnLspActor {UserState : Type} (config : LspConfig UserState) (vfs : VfsActor.VfsRef) (outputChannel : Transport.OutputChannel) (pendingResponses : Server.Receiver.PendingResponses) (userStateRef : IO.Ref UserState) : IO (Actor.Actor (LspMsg UserState) (LspState UserState) × LspRef UserState)

Spawn the LSP actor

Equations

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

Config Builder

def Lapis.Concurrent.LspActor.LspConfig.new {UserState : Type} (name : String) : LspConfig UserState

Create a new LSP config

Equations

• Lapis.Concurrent.LspActor.LspConfig.new name = { name := name }

def Lapis.Concurrent.LspActor.LspConfig.withVersion {UserState : Type} (config : LspConfig UserState) (version : String) : LspConfig UserState

Set version

Equations

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

def Lapis.Concurrent.LspActor.LspConfig.withCapabilities {UserState : Type} (config : LspConfig UserState) (caps : Protocol.Capabilities.ServerCapabilities) : LspConfig UserState

Set capabilities

Equations

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

def Lapis.Concurrent.LspActor.LspConfig.onRequest {Params : Type u_1} {Result UserState : Type} [Lean.FromJson Params] [Lean.ToJson Result] (config : LspConfig UserState) (method : String) (handler : RequestContext UserState → Params → IO Result) : LspConfig UserState

Add a request handler

Equations

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

def Lapis.Concurrent.LspActor.LspConfig.onRequestOpt {Params : Type u_1} {Result UserState : Type} [Lean.FromJson Params] [Lean.ToJson Result] (config : LspConfig UserState) (method : String) (handler : RequestContext UserState → Params → IO (Option Result)) : LspConfig UserState

Add a request handler that can return null

Equations

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

def Lapis.Concurrent.LspActor.LspConfig.onNotification {Params : Type u_1} {UserState : Type} [Lean.FromJson Params] (config : LspConfig UserState) (method : String) (handler : RequestContext UserState → Params → IO Unit) : LspConfig UserState

Add a notification handler

Equations

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

def Lapis.Concurrent.LspActor.LspConfig.withMaxConcurrentRequests {UserState : Type} (config : LspConfig UserState) (n : Nat) : LspConfig UserState

Set max concurrent requests

Equations

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

def Lapis.Concurrent.LspActor.LspConfig.onInitialize {UserState : Type} (config : LspConfig UserState) (hook : RequestContext UserState → Protocol.Messages.InitializeParams → IO Unit) : LspConfig UserState

Equations

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