Server Runtime

structure Lapis.Concurrent.Dispatcher.ServerRuntime (UserState : Type) : Type

Complete server runtime with all actors

• vfsActor : Actor.Actor VfsActor.VfsMsg VfsActor.VfsState

  VFS actor for document management

• vfs : VfsActor.VfsRef

  VFS reference for sending messages

• lspActor : Actor.Actor (LspActor.LspMsg UserState) (LspActor.LspState UserState)

  LSP actor for request handling

• lsp : LspActor.LspRef UserState

  LSP reference for sending messages

• outputChannel : Transport.OutputChannel

  Output channel for responses

• pendingResponses : Server.Receiver.PendingResponses

  Pending responses for server-initiated requests

• userStateRef : IO.Ref UserState

  User state reference (for notifications that need to update it)

def Lapis.Concurrent.Dispatcher.ServerRuntime.getUserState {UserState : Type} (rt : ServerRuntime UserState) : IO UserState

Get current user state

Equations

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

def Lapis.Concurrent.Dispatcher.ServerRuntime.modifyUserState {UserState : Type} (rt : ServerRuntime UserState) (f : UserState → UserState) : IO Unit

Modify user state

Equations

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

def Lapis.Concurrent.Dispatcher.ServerRuntime.setUserState {UserState : Type} (rt : ServerRuntime UserState) (state : UserState) : IO Unit

Set user state

Equations

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

def Lapis.Concurrent.Dispatcher.ServerRuntime.shutdown {UserState : Type} (rt : ServerRuntime UserState) : IO Unit

Shutdown all actors

Equations

• rt.shutdown = do rt.lsp.shutdown rt.vfs.shutdown rt.lspActor.join rt.vfsActor.join

Message Routing

Main Loop

def Lapis.Concurrent.Dispatcher.runMainLoop {T UserState : Type} [Transport.Transport T] (transport : T) (rt : ServerRuntime UserState) : IO Unit

The main message loop - reads from transport and routes to actors

Equations

• Lapis.Concurrent.Dispatcher.runMainLoop transport rt = Lapis.Concurrent.Dispatcher.runMainLoop.loop transport rt

partial def Lapis.Concurrent.Dispatcher.runMainLoop.loop {T UserState : Type} [Transport.Transport T] (transport : T) (rt : ServerRuntime UserState) : IO Unit

Server Startup

def Lapis.Concurrent.Dispatcher.createRuntime {T UserState : Type} [Transport.Transport T] (transport : T) (config : LspActor.LspConfig UserState) (initialState : UserState) : IO (ServerRuntime UserState)

Create and start the server runtime

Equations

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

def Lapis.Concurrent.Dispatcher.runServer {T UserState : Type} [Transport.Transport T] (transport : T) (config : LspActor.LspConfig UserState) (initialState : UserState) : IO Unit

Run the server with the given configuration

Equations

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

def Lapis.Concurrent.Dispatcher.runStdio {UserState : Type} (config : LspActor.LspConfig UserState) (initialState : UserState) : IO Unit

Run the server on stdio

Equations

• Lapis.Concurrent.Dispatcher.runStdio config initialState = do let transport ← Lapis.Transport.Stdio.create Lapis.Concurrent.Dispatcher.runServer transport config initialState