@[reducible, inline]

abbrev Lapis.Server.Registration.RegistrationId : Type

A unique registration ID

Equations

• Lapis.Server.Registration.RegistrationId = String

structure Lapis.Server.Registration.Registration : Type

A registration for a capability

• id : RegistrationId
• method : String
• registerOptions : Option Lean.Json

def Lapis.Server.Registration.instInhabitedRegistration.default : Registration

Equations

• Lapis.Server.Registration.instInhabitedRegistration.default = { id := default, method := default, registerOptions := default }

instance Lapis.Server.Registration.instInhabitedRegistration : Inhabited Registration

Equations

• Lapis.Server.Registration.instInhabitedRegistration = { default := Lapis.Server.Registration.instInhabitedRegistration.default }

instance Lapis.Server.Registration.instToJsonRegistration : Lean.ToJson Registration

Equations

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

instance Lapis.Server.Registration.instFromJsonRegistration : Lean.FromJson Registration

Equations

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

structure Lapis.Server.Registration.Unregistration : Type

Unregistration for a capability

• id : RegistrationId
• method : String

def Lapis.Server.Registration.instInhabitedUnregistration.default : Unregistration

Equations

• Lapis.Server.Registration.instInhabitedUnregistration.default = { id := default, method := default }

instance Lapis.Server.Registration.instInhabitedUnregistration : Inhabited Unregistration

Equations

• Lapis.Server.Registration.instInhabitedUnregistration = { default := Lapis.Server.Registration.instInhabitedUnregistration.default }

instance Lapis.Server.Registration.instToJsonUnregistration : Lean.ToJson Unregistration

Equations

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

structure Lapis.Server.Registration.RegistrationParams : Type

Parameters for client/registerCapability

• registrations : Array Registration

instance Lapis.Server.Registration.instInhabitedRegistrationParams : Inhabited RegistrationParams

Equations

• Lapis.Server.Registration.instInhabitedRegistrationParams = { default := Lapis.Server.Registration.instInhabitedRegistrationParams.default }

def Lapis.Server.Registration.instInhabitedRegistrationParams.default : RegistrationParams

Equations

• Lapis.Server.Registration.instInhabitedRegistrationParams.default = { registrations := default }

instance Lapis.Server.Registration.instToJsonRegistrationParams : Lean.ToJson RegistrationParams

Equations

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

structure Lapis.Server.Registration.UnregistrationParams : Type

Parameters for client/unregisterCapability

• unregistrations : Array Unregistration

def Lapis.Server.Registration.instInhabitedUnregistrationParams.default : UnregistrationParams

Equations

• Lapis.Server.Registration.instInhabitedUnregistrationParams.default = { unregistrations := default }

instance Lapis.Server.Registration.instInhabitedUnregistrationParams : Inhabited UnregistrationParams

Equations

• Lapis.Server.Registration.instInhabitedUnregistrationParams = { default := Lapis.Server.Registration.instInhabitedUnregistrationParams.default }

instance Lapis.Server.Registration.instToJsonUnregistrationParams : Lean.ToJson UnregistrationParams

Equations

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

inductive Lapis.Server.Registration.WatchKind : Type

Kind of file events to watch

• create : WatchKind
• change : WatchKind
• delete : WatchKind

instance Lapis.Server.Registration.instInhabitedWatchKind : Inhabited WatchKind

Equations

• Lapis.Server.Registration.instInhabitedWatchKind = { default := Lapis.Server.Registration.instInhabitedWatchKind.default }

def Lapis.Server.Registration.instInhabitedWatchKind.default : WatchKind

Equations

• Lapis.Server.Registration.instInhabitedWatchKind.default = Lapis.Server.Registration.WatchKind.create

instance Lapis.Server.Registration.instBEqWatchKind : BEq WatchKind

Equations

• Lapis.Server.Registration.instBEqWatchKind = { beq := Lapis.Server.Registration.instBEqWatchKind.beq }

def Lapis.Server.Registration.instBEqWatchKind.beq : WatchKind → WatchKind → Bool

Equations

• Lapis.Server.Registration.instBEqWatchKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Lapis.Server.Registration.WatchKind.toNat : WatchKind → Nat

Equations

• Lapis.Server.Registration.WatchKind.create.toNat = 1
• Lapis.Server.Registration.WatchKind.change.toNat = 2
• Lapis.Server.Registration.WatchKind.delete.toNat = 4

structure Lapis.Server.Registration.FileSystemWatcher : Type

File system watcher pattern

• globPattern : String
• kind : Option Nat

def Lapis.Server.Registration.instInhabitedFileSystemWatcher.default : FileSystemWatcher

Equations

• Lapis.Server.Registration.instInhabitedFileSystemWatcher.default = { globPattern := default, kind := default }

instance Lapis.Server.Registration.instInhabitedFileSystemWatcher : Inhabited FileSystemWatcher

Equations

• Lapis.Server.Registration.instInhabitedFileSystemWatcher = { default := Lapis.Server.Registration.instInhabitedFileSystemWatcher.default }

instance Lapis.Server.Registration.instToJsonFileSystemWatcher : Lean.ToJson FileSystemWatcher

Equations

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

structure Lapis.Server.Registration.DidChangeWatchedFilesRegistrationOptions : Type

Options for registering file watchers

• watchers : Array FileSystemWatcher

def Lapis.Server.Registration.instInhabitedDidChangeWatchedFilesRegistrationOptions.default : DidChangeWatchedFilesRegistrationOptions

Equations

• Lapis.Server.Registration.instInhabitedDidChangeWatchedFilesRegistrationOptions.default = { watchers := default }

instance Lapis.Server.Registration.instInhabitedDidChangeWatchedFilesRegistrationOptions : Inhabited DidChangeWatchedFilesRegistrationOptions

Equations

• Lapis.Server.Registration.instInhabitedDidChangeWatchedFilesRegistrationOptions = { default := Lapis.Server.Registration.instInhabitedDidChangeWatchedFilesRegistrationOptions.default }

instance Lapis.Server.Registration.instToJsonDidChangeWatchedFilesRegistrationOptions : Lean.ToJson DidChangeWatchedFilesRegistrationOptions

Equations

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

structure Lapis.Server.Registration.DocumentFilter : Type

Document filter for registration

• language : Option String
• scheme : Option String
• pattern : Option String

instance Lapis.Server.Registration.instInhabitedDocumentFilter : Inhabited DocumentFilter

Equations

• Lapis.Server.Registration.instInhabitedDocumentFilter = { default := Lapis.Server.Registration.instInhabitedDocumentFilter.default }

def Lapis.Server.Registration.instInhabitedDocumentFilter.default : DocumentFilter

Equations

• Lapis.Server.Registration.instInhabitedDocumentFilter.default = { language := default, scheme := default, pattern := default }

instance Lapis.Server.Registration.instToJsonDocumentFilter : Lean.ToJson DocumentFilter

Equations

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

@[reducible, inline]

abbrev Lapis.Server.Registration.DocumentSelector : Type

Document selector is an array of filters

Equations

• Lapis.Server.Registration.DocumentSelector = Array Lapis.Server.Registration.DocumentFilter

structure Lapis.Server.Registration.TextDocumentRegistrationOptions : Type

Text document registration options

• documentSelector : DocumentSelector

def Lapis.Server.Registration.instInhabitedTextDocumentRegistrationOptions.default : TextDocumentRegistrationOptions

Equations

• Lapis.Server.Registration.instInhabitedTextDocumentRegistrationOptions.default = { documentSelector := default }

instance Lapis.Server.Registration.instInhabitedTextDocumentRegistrationOptions : Inhabited TextDocumentRegistrationOptions

Equations

• Lapis.Server.Registration.instInhabitedTextDocumentRegistrationOptions = { default := Lapis.Server.Registration.instInhabitedTextDocumentRegistrationOptions.default }

instance Lapis.Server.Registration.instToJsonTextDocumentRegistrationOptions : Lean.ToJson TextDocumentRegistrationOptions

Equations

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

structure Lapis.Server.Registration.RegistrationState : Type

Tracks active capability registrations

• registrations : Std.HashMap String (Array RegistrationId)

  Method to list of registration IDs

• byId : Std.HashMap RegistrationId Registration

  All registrations by ID

structure Lapis.Server.Registration.RegistrationManager : Type

Manages dynamic capability registration

• state : IO.Ref RegistrationState

  Current registration state

• idCounter : Concurrent.AtomicCounter

  Counter for generating unique IDs

• outputChannel : Transport.OutputChannel

  Output channel for sending requests

• pendingResponses : Receiver.PendingResponses

  Pending responses

def Lapis.Server.Registration.RegistrationManager.new (outputChannel : Transport.OutputChannel) (pendingResponses : Receiver.PendingResponses) : IO RegistrationManager

Create a new registration manager

Equations

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

def Lapis.Server.Registration.RegistrationManager.generateId (rm : RegistrationManager) (pfx : String := "reg") : IO RegistrationId

Generate a unique registration ID

Equations

• rm.generateId pfx = do let n ← rm.idCounter.incrementAndGet pure (toString pfx ++ toString "-" ++ toString n)

def Lapis.Server.Registration.RegistrationManager.register (rm : RegistrationManager) (method : String) (options : Option Lean.Json := none) : IO (Option RegistrationId)

Register a capability

Equations

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

def Lapis.Server.Registration.RegistrationManager.unregister (rm : RegistrationManager) (id : RegistrationId) : IO Bool

Unregister a capability by ID

Equations

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

def Lapis.Server.Registration.RegistrationManager.unregisterAll (rm : RegistrationManager) (method : String) : IO Bool

Unregister all capabilities for a method

Equations

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

def Lapis.Server.Registration.RegistrationManager.isRegistered (rm : RegistrationManager) (method : String) : IO Bool

Check if a method has any active registrations

Equations

• rm.isRegistered method = do let s ← ST.Ref.get rm.state have ids : Array Lapis.Server.Registration.RegistrationId := s.registrations.getD method #[] pure (decide (ids.size > 0))

def Lapis.Server.Registration.RegistrationManager.getRegistrations (rm : RegistrationManager) (method : String) : IO (Array RegistrationId)

Get all registration IDs for a method

Equations

• rm.getRegistrations method = do let s ← ST.Ref.get rm.state pure (s.registrations.getD method #[])

def Lapis.Server.Registration.RegistrationManager.registerFileWatchers (rm : RegistrationManager) (patterns : Array String) (watchKinds : Option Nat := none) : IO (Option RegistrationId)

Register file watchers

Equations

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

def Lapis.Server.Registration.RegistrationManager.registerFileWatcher (rm : RegistrationManager) (pattern : String) (watchKinds : Option Nat := none) : IO (Option RegistrationId)

Register a single file watcher

Equations

• rm.registerFileWatcher pattern watchKinds = rm.registerFileWatchers #[pattern] watchKinds

def Lapis.Server.Registration.RegistrationManager.mkWatchKind (create change delete : Bool) : Nat

Create a watch kind bitmask

Equations

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

def Lapis.Server.Registration.RegistrationManager.registerForLanguages (rm : RegistrationManager) (method : String) (languages : Array String) (additionalOptions : Option Lean.Json := none) : IO (Option RegistrationId)

Register a text document capability for specific languages

Equations

• One or more equations did not get rendered due to their size.
• rm.registerForLanguages method languages = rm.register method (some (Lean.toJson { documentSelector := Array.map (fun (lang : String) => { language := some lang }) languages }))
• rm.registerForLanguages method languages (some addl✝) = rm.register method (some (Lean.toJson { documentSelector := Array.map (fun (lang : String) => { language := some lang }) languages }))

def Lapis.Server.Registration.RegistrationManager.registerForScheme (rm : RegistrationManager) (method scheme : String) : IO (Option RegistrationId)

Register a text document capability for a file scheme

Equations

• rm.registerForScheme method scheme = rm.register method (some (Lean.toJson { documentSelector := #[{ scheme := some scheme }] }))