Document Snapshot

structure Lapis.Concurrent.VfsActor.DocumentSnapshot : Type

An immutable snapshot of a document for use by request handlers. This can be freely shared across threads.

• uri : String
• languageId : String
• version : Int
• content : String
• lineCount : Nat

def Lapis.Concurrent.VfsActor.instInhabitedDocumentSnapshot.default : DocumentSnapshot

Equations

• Lapis.Concurrent.VfsActor.instInhabitedDocumentSnapshot.default = { uri := default, languageId := default, version := default, content := default, lineCount := default }

instance Lapis.Concurrent.VfsActor.instInhabitedDocumentSnapshot : Inhabited DocumentSnapshot

Equations

• Lapis.Concurrent.VfsActor.instInhabitedDocumentSnapshot = { default := Lapis.Concurrent.VfsActor.instInhabitedDocumentSnapshot.default }

def Lapis.Concurrent.VfsActor.DocumentSnapshot.getLine (snap : DocumentSnapshot) (line : Nat) : Option String

Get a line from the snapshot

Equations

• snap.getLine line = if h : line < (snap.content.splitOn "\n").length then some (snap.content.splitOn "\n")[line] else none

def Lapis.Concurrent.VfsActor.DocumentSnapshot.getText (snap : DocumentSnapshot) (startLine startChar endLine endChar : Nat) : Option String

Get text in a range

Equations

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

VFS Messages

inductive Lapis.Concurrent.VfsActor.VfsMsg : Type

Messages that the VFS actor can receive

• openDocument (params : Protocol.Messages.DidOpenTextDocumentParams) : VfsMsg

  Open a new document

• closeDocument (params : Protocol.Messages.DidCloseTextDocumentParams) : VfsMsg

  Close a document

• changeDocument (params : Protocol.Messages.DidChangeTextDocumentParams) : VfsMsg

  Apply changes to a document

• getSnapshot (uri : Protocol.Types.DocumentUri) (replyTo : Channel.Oneshot (Option DocumentSnapshot)) : VfsMsg

  Request a snapshot of a document

• getContent (uri : Protocol.Types.DocumentUri) (replyTo : Channel.Oneshot (Option String)) : VfsMsg

  Request content of a document

• getLine (uri : Protocol.Types.DocumentUri) (line : Nat) (replyTo : Channel.Oneshot (Option String)) : VfsMsg

  Request a specific line

• getWordAt (uri : Protocol.Types.DocumentUri) (pos : Protocol.Types.Position) (replyTo : Channel.Oneshot (Option String)) : VfsMsg

  Request word at position

• positionToOffset (uri : Protocol.Types.DocumentUri) (pos : Protocol.Types.Position) (replyTo : Channel.Oneshot (Option Nat)) : VfsMsg

  Request position to offset conversion

• offsetToPosition (uri : Protocol.Types.DocumentUri) (offset : Nat) (replyTo : Channel.Oneshot (Option Protocol.Types.Position)) : VfsMsg

  Request offset to position conversion

• getOpenDocuments (replyTo : Channel.Oneshot (List String)) : VfsMsg

  Get list of open documents

• hasDocument (uri : Protocol.Types.DocumentUri) (replyTo : Channel.Oneshot Bool) : VfsMsg

  Check if document exists

• shutdown : VfsMsg

  Shutdown the VFS actor

VFS Actor State

structure Lapis.Concurrent.VfsActor.VfsState : Type

Internal state of the VFS actor

• store : VFS.DocumentStore

VFS Actor Reference

structure Lapis.Concurrent.VfsActor.VfsRef : Type

A handle to communicate with the VFS actor

• ref : Actor.ActorRef VfsMsg

def Lapis.Concurrent.VfsActor.VfsRef.openDocument (vfs : VfsRef) (params : Protocol.Messages.DidOpenTextDocumentParams) : IO Unit

Open a document (fire and forget)

Equations

• vfs.openDocument params = vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.openDocument params)

def Lapis.Concurrent.VfsActor.VfsRef.closeDocument (vfs : VfsRef) (params : Protocol.Messages.DidCloseTextDocumentParams) : IO Unit

Close a document (fire and forget)

Equations

• vfs.closeDocument params = vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.closeDocument params)

def Lapis.Concurrent.VfsActor.VfsRef.changeDocument (vfs : VfsRef) (params : Protocol.Messages.DidChangeTextDocumentParams) : IO Unit

Apply changes to a document (fire and forget)

Equations

• vfs.changeDocument params = vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.changeDocument params)

def Lapis.Concurrent.VfsActor.VfsRef.getSnapshot (vfs : VfsRef) (uri : Protocol.Types.DocumentUri) : IO (Option DocumentSnapshot)

Get a snapshot of a document (blocking request-response)

Equations

• vfs.getSnapshot uri = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.getSnapshot uri reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.getContent (vfs : VfsRef) (uri : Protocol.Types.DocumentUri) : IO (Option String)

Get document content

Equations

• vfs.getContent uri = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.getContent uri reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.getLine (vfs : VfsRef) (uri : Protocol.Types.DocumentUri) (line : Nat) : IO (Option String)

Get a specific line

Equations

• vfs.getLine uri line = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.getLine uri line reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.getWordAt (vfs : VfsRef) (uri : Protocol.Types.DocumentUri) (pos : Protocol.Types.Position) : IO (Option String)

Get word at position

Equations

• vfs.getWordAt uri pos = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.getWordAt uri pos reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.positionToOffset (vfs : VfsRef) (uri : Protocol.Types.DocumentUri) (pos : Protocol.Types.Position) : IO (Option Nat)

Convert position to byte offset

Equations

• vfs.positionToOffset uri pos = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.positionToOffset uri pos reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.offsetToPosition (vfs : VfsRef) (uri : Protocol.Types.DocumentUri) (offset : Nat) : IO (Option Protocol.Types.Position)

Convert byte offset to position

Equations

• vfs.offsetToPosition uri offset = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.offsetToPosition uri offset reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.getOpenDocuments (vfs : VfsRef) : IO (List String)

Get list of open document URIs

Equations

• vfs.getOpenDocuments = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.getOpenDocuments reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.hasDocument (vfs : VfsRef) (uri : Protocol.Types.DocumentUri) : IO Bool

Check if a document is open

Equations

• vfs.hasDocument uri = do let reply ← Lapis.Concurrent.Channel.Oneshot.new vfs.ref.send (Lapis.Concurrent.VfsActor.VfsMsg.hasDocument uri reply) reply.recv

def Lapis.Concurrent.VfsActor.VfsRef.shutdown (vfs : VfsRef) : IO Unit

Request shutdown

Equations

• vfs.shutdown = vfs.ref.send Lapis.Concurrent.VfsActor.VfsMsg.shutdown

Helper Functions

VFS Actor Implementation

def Lapis.Concurrent.VfsActor.spawnVfsActor : IO (Actor.Actor VfsMsg VfsState × VfsRef)

Spawn the VFS actor

Equations

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