structure Lapis.VFS.LineIndex.LineEntry : Type

A line entry stores the byte length of a single line (including newline if present)

• byteLength : Nat

instance Lapis.VFS.LineIndex.instInhabitedLineEntry : Inhabited LineEntry

Equations

• Lapis.VFS.LineIndex.instInhabitedLineEntry = { default := Lapis.VFS.LineIndex.instInhabitedLineEntry.default }

def Lapis.VFS.LineIndex.instInhabitedLineEntry.default : LineEntry

Equations

• Lapis.VFS.LineIndex.instInhabitedLineEntry.default = { byteLength := default }

instance Lapis.VFS.LineIndex.instReprLineEntry : Repr LineEntry

Equations

• Lapis.VFS.LineIndex.instReprLineEntry = { reprPrec := Lapis.VFS.LineIndex.instReprLineEntry.repr }

def Lapis.VFS.LineIndex.instReprLineEntry.repr : LineEntry → Nat → Std.Format

Equations

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

instance Lapis.VFS.LineIndex.instMeasurableLineEntry : FingerTree.Measurable LineEntry

Equations

• Lapis.VFS.LineIndex.instMeasurableLineEntry = { measure := fun (entry : Lapis.VFS.LineIndex.LineEntry) => { bytes := entry.byteLength, utf16Units := 0, lines := 1 } }

structure Lapis.VFS.LineIndex.LineIndex : Type

Line index using a finger tree of line entries

• lines : FingerTree.FingerTree LineEntry

  Finger tree of line entries, one per line

• docLength : Nat

  Total byte length of the document

def Lapis.VFS.LineIndex.instInhabitedLineIndex.default : LineIndex

Equations

• Lapis.VFS.LineIndex.instInhabitedLineIndex.default = { lines := default, docLength := default }

instance Lapis.VFS.LineIndex.instInhabitedLineIndex : Inhabited LineIndex

Equations

• Lapis.VFS.LineIndex.instInhabitedLineIndex = { default := Lapis.VFS.LineIndex.instInhabitedLineIndex.default }

def Lapis.VFS.LineIndex.LineIndex.empty : LineIndex

Create an empty line index (single empty line)

Equations

• Lapis.VFS.LineIndex.LineIndex.empty = { lines := Lapis.VFS.FingerTree.FingerTree.single { byteLength := 0 }, docLength := 0 }

def Lapis.VFS.LineIndex.LineIndex.lineCount (idx : LineIndex) : Nat

Get the number of lines

Equations

• idx.lineCount = idx.lines.measure.lines

def Lapis.VFS.LineIndex.LineIndex.isValidLine (idx : LineIndex) (line : Nat) : Bool

Check if a line number is valid

Equations

• idx.isValidLine line = decide (line < idx.lineCount)

def Lapis.VFS.LineIndex.LineIndex.build (content : String) : LineIndex

Build a complete line index from document content

Equations

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

@[irreducible]

def Lapis.VFS.LineIndex.LineIndex.build.buildEntries (s : String) (pos lineStart : Nat) (acc : Array LineEntry) : Array LineEntry

Equations

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

def Lapis.VFS.LineIndex.LineIndex.getLineOffset? (idx : LineIndex) (line : Nat) : Option Nat

Get byte offset for the start of a line - O(log n)

Equations

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

def Lapis.VFS.LineIndex.LineIndex.getLineByteRange (idx : LineIndex) (line : Nat) : Option (Nat × Nat)

Get the byte range for a line - O(log n)

Equations

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

def Lapis.VFS.LineIndex.LineIndex.findLineForOffset (idx : LineIndex) (byteOffset : Nat) : Nat

Find which line a byte offset falls on - O(log n)

Equations

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

def Lapis.VFS.LineIndex.LineIndex.applyEdit (idx : LineIndex) (startByte oldLength : Nat) (newText : String) (newDocLength : Nat) : LineIndex

Apply an incremental edit to the line index - O(log n)

Parameters:

• startByte: byte offset where the edit starts
• oldLength: number of bytes removed (0 for pure insert)
• newText: the text being inserted
• newDocLength: total document length after the edit

Equations

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

def Lapis.VFS.LineIndex.LineIndex.applyEdit.rebuildTree (tree : FingerTree.FingerTree LineEntry) (startLine endLine : Nat) (newEntries : Array LineEntry) : FingerTree.FingerTree LineEntry

Equations

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