Re-exports

Document Store

structure Lapis.VFS.DocumentStore : Type

A store of open documents, keyed by URI

• documents : IO.Ref (Std.HashMap String Document)

def Lapis.VFS.DocumentStore.empty : IO DocumentStore

Create an empty document store

Equations

• Lapis.VFS.DocumentStore.empty = do let docs ← liftM (IO.mkRef ∅) pure { documents := docs }

def Lapis.VFS.DocumentStore.get (store : DocumentStore) (uri : String) : IO (Option Document)

Get a document by URI

Equations

• store.get uri = do let docs ← ST.Ref.get store.documents pure (docs.get? uri)

def Lapis.VFS.DocumentStore.contains (store : DocumentStore) (uri : String) : IO Bool

Check if a document exists

Equations

• store.contains uri = do let docs ← ST.Ref.get store.documents pure (docs.contains uri)

Document Lifecycle

def Lapis.VFS.DocumentStore.openDocument (store : DocumentStore) (uri languageId : String) (version : Int) (content : String) : IO Unit

Open a new document

Equations

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

def Lapis.VFS.DocumentStore.closeDocument (store : DocumentStore) (uri : String) : IO Unit

Close a document

Equations

• store.closeDocument uri = ST.Ref.modify store.documents fun (docs : Std.HashMap String Lapis.VFS.Document) => docs.erase uri

def Lapis.VFS.DocumentStore.updateVersion (store : DocumentStore) (uri : String) (version : Int) : IO Unit

Update document version (without content change)

Equations

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

Editing

def Lapis.VFS.DocumentStore.applyEdit (store : DocumentStore) (uri : String) (range : LspRange) (newText : String) (newVersion : Int) : IO Unit

Apply a text edit to a document

Equations

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

def Lapis.VFS.DocumentStore.applyEdits (store : DocumentStore) (uri : String) (edits : List (LspRange × String)) (newVersion : Int) : IO Unit

Apply multiple edits to a document (edits should be in reverse document order)

Equations

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

def Lapis.VFS.DocumentStore.setContent (store : DocumentStore) (uri content : String) (newVersion : Int) : IO Unit

Replace entire document content

Equations

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

Reading

def Lapis.VFS.DocumentStore.getText (store : DocumentStore) (uri : String) (range : LspRange) : IO (Option String)

Get text in a range

Equations

• store.getText uri range = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (doc.getText range)

def Lapis.VFS.DocumentStore.getLine (store : DocumentStore) (uri : String) (line : Nat) : IO (Option String)

Get a specific line

Equations

• store.getLine uri line = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (doc.getLine line)

def Lapis.VFS.DocumentStore.getContent (store : DocumentStore) (uri : String) : IO (Option String)

Get full document content

Equations

• store.getContent uri = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (some doc.getContent)

def Lapis.VFS.DocumentStore.getVersion (store : DocumentStore) (uri : String) : IO (Option Int)

Get document version

Equations

• store.getVersion uri = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (some doc.version)

def Lapis.VFS.DocumentStore.getLineCount (store : DocumentStore) (uri : String) : IO (Option Nat)

Get document line count

Equations

• store.getLineCount uri = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (some doc.lineCount)

def Lapis.VFS.DocumentStore.getByteLength (store : DocumentStore) (uri : String) : IO (Option Nat)

Get document byte length

Equations

• store.getByteLength uri = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (some doc.byteLength)

Position Conversion

def Lapis.VFS.DocumentStore.positionToOffset (store : DocumentStore) (uri : String) (pos : LspPosition) : IO (Option Nat)

Convert LSP position to byte offset

Equations

• store.positionToOffset uri pos = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (doc.positionToOffset pos)

def Lapis.VFS.DocumentStore.offsetToPosition (store : DocumentStore) (uri : String) (offset : Nat) : IO (Option LspPosition)

Convert byte offset to LSP position

Equations

• store.offsetToPosition uri offset = do let __do_lift ← store.get uri match __do_lift with | none => pure none | some doc => pure (some (doc.offsetToPosition offset))

def Lapis.VFS.DocumentStore.byteRangeToLspRange (store : DocumentStore) (uri : String) (startByte endByte : Nat) : IO (Option LspRange)

Convert a byte range to an LSP range

Equations

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

def Lapis.VFS.DocumentStore.lspRangeToByteRange (store : DocumentStore) (uri : String) (range : LspRange) : IO (Option (Nat × Nat))

Convert an LSP range to a byte range

Equations

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

Snapshots

def Lapis.VFS.DocumentStore.createSnapshot (store : DocumentStore) (uri : String) (reason : SnapshotReason) : IO (Option SnapshotId)

Create a snapshot of the current document state

Equations

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

def Lapis.VFS.DocumentStore.acquireSnapshot (store : DocumentStore) (uri : String) (id : SnapshotId) : IO (Option PieceTable.PieceTableState)

Acquire a snapshot (increment reference count)

Equations

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

def Lapis.VFS.DocumentStore.releaseSnapshot (store : DocumentStore) (uri : String) (id : SnapshotId) : IO Unit

Release a snapshot (decrement reference count)

Equations

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

def Lapis.VFS.DocumentStore.pruneSnapshots (store : DocumentStore) (uri : String) : IO Unit

Prune unreferenced snapshots

Equations

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

def Lapis.VFS.DocumentStore.rebuildLineIndex (store : DocumentStore) (uri : String) : IO Unit

Rebuild document line index

Equations

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

def Lapis.VFS.DocumentStore.getOpenDocuments (store : DocumentStore) : IO (List String)

Get list of all open document URIs

Equations

• store.getOpenDocuments = do let docs ← ST.Ref.get store.documents pure docs.keys

def Lapis.VFS.DocumentStore.modify (store : DocumentStore) (uri : String) (f : Document → Document) : IO Unit

Modify a document with a function

Equations

• store.modify uri f = ST.Ref.modify store.documents fun (docs : Std.HashMap String Lapis.VFS.Document) => match docs.get? uri with | none => docs | some doc => docs.insert uri (f doc)

Convenience Functions

def Lapis.VFS.zeroPosition : LspPosition

Create a zero position

Equations

• Lapis.VFS.zeroPosition = Lapis.VFS.Position.LspPosition.zero

def Lapis.VFS.emptyRange : LspRange

Create an empty range

Equations

• Lapis.VFS.emptyRange = Lapis.VFS.Position.LspRange.empty

def Lapis.VFS.pointRange (pos : LspPosition) : LspRange

Create a range at a single point

Equations

• Lapis.VFS.pointRange pos = Lapis.VFS.Position.LspRange.point pos

def Lapis.VFS.mkPosition (line character : Nat) : LspPosition

Create a position from line and character

Equations

• Lapis.VFS.mkPosition line character = { line := line, character := character }

def Lapis.VFS.mkRange (start «end» : LspPosition) : LspRange

Create a range from start and end positions

Equations

• Lapis.VFS.mkRange start «end» = { start := start, «end» := «end» }

def Lapis.VFS.mkRangeFromCoords (startLine startChar endLine endChar : Nat) : LspRange

Create a range from line/character coordinates

Equations

• Lapis.VFS.mkRangeFromCoords startLine startChar endLine endChar = { start := { line := startLine, character := startChar }, «end» := { line := endLine, character := endChar } }