TermColor.Terminal.Buffer

Pure cell storage and cell-level diffing. The line renderer remains the default Screen backend; this backend exists for applications that need positioned, partially changing content.

structure TermColor.Terminal.Cell : Type

One terminal cell. A continuation cell belongs to the preceding wide glyph.

• glyph : String
• style : Style
• link : Option String
• continuation : Bool

def TermColor.Terminal.instBEqCell.beq : Cell → Cell → Bool

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Terminal.instBEqCell.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instBEqCell : BEq Cell

Equations

• TermColor.Terminal.instBEqCell = { beq := TermColor.Terminal.instBEqCell.beq }

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqCell : DecidableEq Cell

Equations

• TermColor.Terminal.instDecidableEqCell = TermColor.Terminal.instDecidableEqCell.decEq

def TermColor.Terminal.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprCell : Repr Cell

Equations

• TermColor.Terminal.instReprCell = { reprPrec := TermColor.Terminal.instReprCell.repr }

def TermColor.Terminal.instReprCell.repr : Cell → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedCell : Inhabited Cell

Equations

• TermColor.Terminal.instInhabitedCell = { default := TermColor.Terminal.instInhabitedCell.default }

def TermColor.Terminal.blankCell : Cell

Equations

• TermColor.Terminal.blankCell = { }

structure TermColor.Terminal.Buffer : Type

A fixed-size pure terminal surface. Coordinates are zero-based internally.

• width : Nat
• height : Nat
• cells : Array Cell

def TermColor.Terminal.instBEqBuffer.beq : Buffer → Buffer → Bool

Equations

• TermColor.Terminal.instBEqBuffer.beq { width := a, height := a_1, cells := a_2 } { width := b, height := b_1, cells := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• TermColor.Terminal.instBEqBuffer.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instBEqBuffer : BEq Buffer

Equations

• TermColor.Terminal.instBEqBuffer = { beq := TermColor.Terminal.instBEqBuffer.beq }

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqBuffer : DecidableEq Buffer

Equations

• TermColor.Terminal.instDecidableEqBuffer = TermColor.Terminal.instDecidableEqBuffer.decEq

def TermColor.Terminal.instDecidableEqBuffer.decEq (x✝ x✝¹ : Buffer) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprBuffer : Repr Buffer

Equations

• TermColor.Terminal.instReprBuffer = { reprPrec := TermColor.Terminal.instReprBuffer.repr }

def TermColor.Terminal.instReprBuffer.repr : Buffer → Nat → Std.Format

Equations

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

def TermColor.Terminal.Buffer.empty (width height : Nat) : Buffer

Equations

• TermColor.Terminal.Buffer.empty width height = { width := width, height := height, cells := Array.replicate (width * height) TermColor.Terminal.blankCell }

def TermColor.Terminal.Buffer.get (buffer : Buffer) (column row : Nat) : Cell

Equations

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

def TermColor.Terminal.Buffer.set (buffer : Buffer) (column row : Nat) (cell : Cell) : Buffer

Equations

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

def TermColor.Terminal.Buffer.writeText (buffer : Buffer) (column row : Nat) (text : Text) : Buffer

Write styled text at a zero-based cell coordinate, clipping at the surface boundary.

Equations

• buffer.writeText column row text = (TermColor.Terminal.Buffer.writeSegments✝ buffer column row text.segments).fst

def TermColor.Terminal.Buffer.fromText (size : Size) (text : Text) : Buffer

Render a wrapped text value into a fixed-size surface.

Equations

• TermColor.Terminal.Buffer.fromText size text = (TermColor.Terminal.Buffer.empty size.columns size.rows).writeText 0 0 (TermColor.Layout.wrapLines (max 1 size.columns) text)

def TermColor.Terminal.Buffer.cellText (cell : Cell) : Text

Equations

• TermColor.Terminal.Buffer.cellText cell = if cell.continuation = true then TermColor.Text.empty else { segments := [{ text := cell.glyph, style := cell.style, link := cell.link }] }

def TermColor.Terminal.Buffer.rowText (buffer : Buffer) (row : Nat) : Text

Equations

• buffer.rowText row = TermColor.Text.concat (List.map (fun (column : Nat) => TermColor.Terminal.Buffer.cellText (buffer.get column row)) (List.range buffer.width))

def TermColor.Terminal.Buffer.rowTextRange (buffer : Buffer) (row start finish : Nat) : Text

Equations

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

def TermColor.Terminal.Buffer.toText (buffer : Buffer) : Text

Equations

• buffer.toText = TermColor.Layout.joinLines (List.map (fun (x : Nat) => buffer.rowText x) (List.range buffer.height))

structure TermColor.Terminal.BufferScreen : Type

• previous : Option Buffer

@[instance_reducible]

instance TermColor.Terminal.instBEqBufferScreen : BEq BufferScreen

Equations

• TermColor.Terminal.instBEqBufferScreen = { beq := TermColor.Terminal.instBEqBufferScreen.beq }

def TermColor.Terminal.instBEqBufferScreen.beq : BufferScreen → BufferScreen → Bool

Equations

• TermColor.Terminal.instBEqBufferScreen.beq { previous := a } { previous := b } = (a == b)
• TermColor.Terminal.instBEqBufferScreen.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqBufferScreen : DecidableEq BufferScreen

Equations

• TermColor.Terminal.instDecidableEqBufferScreen = TermColor.Terminal.instDecidableEqBufferScreen.decEq

def TermColor.Terminal.instDecidableEqBufferScreen.decEq (x✝ x✝¹ : BufferScreen) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqBufferScreen.decEq { previous := a } { previous := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.Terminal.instReprBufferScreen : Repr BufferScreen

Equations

• TermColor.Terminal.instReprBufferScreen = { reprPrec := TermColor.Terminal.instReprBufferScreen.repr }

def TermColor.Terminal.instReprBufferScreen.repr : BufferScreen → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedBufferScreen : Inhabited BufferScreen

Equations

• TermColor.Terminal.instInhabitedBufferScreen = { default := TermColor.Terminal.instInhabitedBufferScreen.default }

def TermColor.Terminal.BufferScreen.empty : BufferScreen

Equations

• TermColor.Terminal.BufferScreen.empty = { }

def TermColor.Terminal.BufferScreen.diffSequence (screen : BufferScreen) (next : Buffer) : Text × BufferScreen

Pure cell-level output and next state. Initial or resized surfaces redraw fully.

Equations

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