TermColor.Layout.Basic: pure styled-text layout

These operations preserve segment styles and never emit ANSI escapes. Rendering remains the responsibility of TermColor.Text.render.

def TermColor.Layout.defaultWidth : Nat

Default fallback for layout that has no terminal width yet.

Equations

• TermColor.Layout.defaultWidth = 80

inductive TermColor.Layout.Alignment : Type

• left : Alignment

  Align content against the left edge.

• right : Alignment

  Align content against the right edge.

• center : Alignment

  Center content within the available width.

def TermColor.Layout.instBEqAlignment.beq : Alignment → Alignment → Bool

Equations

• TermColor.Layout.instBEqAlignment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.Layout.instBEqAlignment : BEq Alignment

Equations

• TermColor.Layout.instBEqAlignment = { beq := TermColor.Layout.instBEqAlignment.beq }

@[instance_reducible]

instance TermColor.Layout.instDecidableEqAlignment : DecidableEq Alignment

Equations

• TermColor.Layout.instDecidableEqAlignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TermColor.Layout.instReprAlignment.repr : Alignment → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Layout.instReprAlignment : Repr Alignment

Equations

• TermColor.Layout.instReprAlignment = { reprPrec := TermColor.Layout.instReprAlignment.repr }

@[instance_reducible]

instance TermColor.Layout.instInhabitedAlignment : Inhabited Alignment

Equations

• TermColor.Layout.instInhabitedAlignment = { default := TermColor.Layout.instInhabitedAlignment.default }

def TermColor.Layout.splitLines (text : Text) : List Text

Split a Text into logical lines on '\n', preserving each segment's style.

The counterpart to joinLines. Callers laying out their own multi-line cells need this to indent or pad continuation lines: columns aligns every column to its width, so a caller that wants no trailing padding on the last column has to split and rejoin itself.

Equations

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

def TermColor.Layout.joinLines : List Text → Text

Join logical lines with newline separators.

Equations

• TermColor.Layout.joinLines [] = TermColor.Text.empty
• TermColor.Layout.joinLines (first :: rest) = List.foldl (fun (result line : TermColor.Text) => result ++ TermColor.Text.plain "\n" ++ line) first rest

def TermColor.Layout.padRight (target : Nat) (text : Text) : Text

Pad every logical line on the right to target columns.

Equations

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

def TermColor.Layout.padLeft (target : Nat) (text : Text) : Text

Pad every logical line on the left to target columns.

Equations

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

def TermColor.Layout.align (target : Nat) (alignment : Alignment) (text : Text) : Text

Align every logical line to target columns.

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Layout.align target TermColor.Layout.Alignment.left text = TermColor.Layout.padRight target text
• TermColor.Layout.align target TermColor.Layout.Alignment.right text = TermColor.Layout.padLeft target text

def TermColor.Layout.truncate (limit : Nat) (text : Text) : Text

Keep at most limit display columns on each logical line.

Equations

• TermColor.Layout.truncate limit text = TermColor.Layout.mapLines✝ (TermColor.Layout.takeWidth✝ limit) text

def TermColor.Layout.wrapLines (limit : Nat) (text : Text) : Text

Wrap every logical line to at most limit display columns. A wide first character may occupy two columns when limit is one, since splitting a character is impossible.

Equations

• TermColor.Layout.wrapLines limit text = TermColor.Layout.joinLines (List.flatMap (TermColor.Layout.wrapLine✝ (max 1 limit)) (TermColor.Layout.splitLines text))

def TermColor.Layout.wrapWords (limit : Nat) (text : Text) : Text

Wrap every logical line to at most limit display columns, breaking at spaces where possible. A word wider than limit is split like wrapLines; spaces at a break are dropped.

Equations

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

def TermColor.Layout.gutter (marker : Text) (indent width : Nat) (body : Text) : Text

Wrap body to width, prefixing its first line with marker and continuations with spaces.

Equations

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

def TermColor.Layout.columns (widths : List Nat) (gap : Nat) (cells : List Text) (alignments : List Alignment := []) (separator : Text := Text.empty) : Text

Lay out one row of styled cells as fixed-width columns. Cells wrap before alignment.

Equations

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

Characters used to draw a box.

structure TermColor.Layout.BoxChars : Type

• topLeft : Char

  Top-left corner.

• topRight : Char

  Top-right corner.

• bottomLeft : Char

  Bottom-left corner.

• bottomRight : Char

  Bottom-right corner.

• horizontal : Char

  Horizontal border character.

• vertical : Char

  Vertical border character.

def TermColor.Layout.instBEqBoxChars.beq : BoxChars → BoxChars → Bool

Equations

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

@[instance_reducible]

instance TermColor.Layout.instBEqBoxChars : BEq BoxChars

Equations

• TermColor.Layout.instBEqBoxChars = { beq := TermColor.Layout.instBEqBoxChars.beq }

def TermColor.Layout.instDecidableEqBoxChars.decEq (x✝ x✝¹ : BoxChars) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Layout.instDecidableEqBoxChars : DecidableEq BoxChars

Equations

• TermColor.Layout.instDecidableEqBoxChars = TermColor.Layout.instDecidableEqBoxChars.decEq

def TermColor.Layout.instReprBoxChars.repr : BoxChars → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Layout.instReprBoxChars : Repr BoxChars

Equations

• TermColor.Layout.instReprBoxChars = { reprPrec := TermColor.Layout.instReprBoxChars.repr }

@[instance_reducible]

instance TermColor.Layout.instInhabitedBoxChars : Inhabited BoxChars

Equations

• TermColor.Layout.instInhabitedBoxChars = { default := TermColor.Layout.instInhabitedBoxChars.default }

def TermColor.Layout.asciiBoxChars : BoxChars

ASCII characters for terminals without Unicode box drawing.

Equations

• TermColor.Layout.asciiBoxChars = { topLeft := '+', topRight := '+', bottomLeft := '+', bottomRight := '+', horizontal := '-', vertical := '|' }

Configuration for box. maxWidth is the outer width, including borders and padding.

structure TermColor.Layout.BoxConfig : Type

• chars : BoxChars

  Characters used for the border.

• borderStyle : Style

  Style applied to border characters.

• padding : Nat

  Number of spaces between the border and content.

• title : Option Text

  Optional one-line title in the top border.

• titleAlignment : Alignment

  Horizontal alignment of the title.

• maxWidth : Option Nat

  Maximum outer width, including borders and padding.

@[instance_reducible]

instance TermColor.Layout.instBEqBoxConfig : BEq BoxConfig

Equations

• TermColor.Layout.instBEqBoxConfig = { beq := TermColor.Layout.instBEqBoxConfig.beq }

def TermColor.Layout.instBEqBoxConfig.beq : BoxConfig → BoxConfig → Bool

Equations

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

@[instance_reducible]

instance TermColor.Layout.instDecidableEqBoxConfig : DecidableEq BoxConfig

Equations

• TermColor.Layout.instDecidableEqBoxConfig = TermColor.Layout.instDecidableEqBoxConfig.decEq

def TermColor.Layout.instDecidableEqBoxConfig.decEq (x✝ x✝¹ : BoxConfig) : Decidable (x✝ = x✝¹)

Equations

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

def TermColor.Layout.instReprBoxConfig.repr : BoxConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Layout.instReprBoxConfig : Repr BoxConfig

Equations

• TermColor.Layout.instReprBoxConfig = { reprPrec := TermColor.Layout.instReprBoxConfig.repr }

@[instance_reducible]

instance TermColor.Layout.instInhabitedBoxConfig : Inhabited BoxConfig

Equations

• TermColor.Layout.instInhabitedBoxConfig = { default := { } }

def TermColor.Layout.boxInnerWidth (config : BoxConfig) (outer : Nat) : Nat

The content width left inside a box with the given outer width.

Equations

• TermColor.Layout.boxInnerWidth config outer = max 1 (outer - 2 - 2 * config.padding)

def TermColor.Layout.box (content : Text) (config : BoxConfig := { }) : Text

Draw a pure text box around styled content. maxWidth limits the outer width when supplied.

Equations

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