TermColor.Widgets.Basic: pure progress and spinner rendering

Widgets own state-to-text rendering. A caller owns timers, terminal width, and output.

structure TermColor.Widgets.ProgressState : Type

State displayed by a progress bar. current is clamped to total when rendered.

• current : Nat
• total : Nat
• label : Text

def TermColor.Widgets.instBEqProgressState.beq : ProgressState → ProgressState → Bool

Equations

• TermColor.Widgets.instBEqProgressState.beq { current := a, total := a_1, label := a_2 } { current := b, total := b_1, label := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• TermColor.Widgets.instBEqProgressState.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Widgets.instBEqProgressState : BEq ProgressState

Equations

• TermColor.Widgets.instBEqProgressState = { beq := TermColor.Widgets.instBEqProgressState.beq }

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqProgressState : DecidableEq ProgressState

Equations

• TermColor.Widgets.instDecidableEqProgressState = TermColor.Widgets.instDecidableEqProgressState.decEq

def TermColor.Widgets.instDecidableEqProgressState.decEq (x✝ x✝¹ : ProgressState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprProgressState : Repr ProgressState

Equations

• TermColor.Widgets.instReprProgressState = { reprPrec := TermColor.Widgets.instReprProgressState.repr }

def TermColor.Widgets.instReprProgressState.repr : ProgressState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedProgressState : Inhabited ProgressState

Equations

• TermColor.Widgets.instInhabitedProgressState = { default := { } }

structure TermColor.Widgets.ProgressConfig : Type

Rendering choices for a progress bar. width is the display width without brackets or suffixes.

• width : Nat
• filledChar : Char
• emptyChar : Char
• filledStyle : Style
• emptyStyle : Style
• percentageStyle : Style
• showPercentage : Bool
• indeterminateWidth : Nat

def TermColor.Widgets.instBEqProgressConfig.beq : ProgressConfig → ProgressConfig → Bool

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instBEqProgressConfig : BEq ProgressConfig

Equations

• TermColor.Widgets.instBEqProgressConfig = { beq := TermColor.Widgets.instBEqProgressConfig.beq }

def TermColor.Widgets.instDecidableEqProgressConfig.decEq (x✝ x✝¹ : ProgressConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqProgressConfig : DecidableEq ProgressConfig

Equations

• TermColor.Widgets.instDecidableEqProgressConfig = TermColor.Widgets.instDecidableEqProgressConfig.decEq

def TermColor.Widgets.instReprProgressConfig.repr : ProgressConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprProgressConfig : Repr ProgressConfig

Equations

• TermColor.Widgets.instReprProgressConfig = { reprPrec := TermColor.Widgets.instReprProgressConfig.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedProgressConfig : Inhabited ProgressConfig

Equations

• TermColor.Widgets.instInhabitedProgressConfig = { default := { } }

def TermColor.Widgets.progressPercent (state : ProgressState) : Nat

Percentage shown by a progress bar. Zero total means no work remains, so it is complete.

Equations

• TermColor.Widgets.progressPercent state = if (state.total == 0) = true then 100 else min 100 (state.current * 100 / state.total)

def TermColor.Widgets.progressBar (config : ProgressConfig) (state : ProgressState) : Text

Render a progress bar as styled text. The caller supplies the desired bar width explicitly.

Equations

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

structure TermColor.Widgets.IndeterminateProgressState : Type

State displayed by an indeterminate progress bar. The frame moves back and forth.

• frame : Nat
• label : Text

@[instance_reducible]

instance TermColor.Widgets.instBEqIndeterminateProgressState : BEq IndeterminateProgressState

Equations

• TermColor.Widgets.instBEqIndeterminateProgressState = { beq := TermColor.Widgets.instBEqIndeterminateProgressState.beq }

def TermColor.Widgets.instBEqIndeterminateProgressState.beq : IndeterminateProgressState → IndeterminateProgressState → Bool

Equations

• TermColor.Widgets.instBEqIndeterminateProgressState.beq { frame := a, label := a_1 } { frame := b, label := b_1 } = (a == b && a_1 == b_1)
• TermColor.Widgets.instBEqIndeterminateProgressState.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqIndeterminateProgressState : DecidableEq IndeterminateProgressState

Equations

• TermColor.Widgets.instDecidableEqIndeterminateProgressState = TermColor.Widgets.instDecidableEqIndeterminateProgressState.decEq

def TermColor.Widgets.instDecidableEqIndeterminateProgressState.decEq (x✝ x✝¹ : IndeterminateProgressState) : Decidable (x✝ = x✝¹)

Equations

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

def TermColor.Widgets.instReprIndeterminateProgressState.repr : IndeterminateProgressState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprIndeterminateProgressState : Repr IndeterminateProgressState

Equations

• TermColor.Widgets.instReprIndeterminateProgressState = { reprPrec := TermColor.Widgets.instReprIndeterminateProgressState.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedIndeterminateProgressState : Inhabited IndeterminateProgressState

Equations

• TermColor.Widgets.instInhabitedIndeterminateProgressState = { default := { } }

def TermColor.Widgets.indeterminateProgressOffset (config : ProgressConfig) (state : IndeterminateProgressState) : Nat

Moving segment offset for an indeterminate progress bar.

Equations

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

def TermColor.Widgets.indeterminateProgressBar (config : ProgressConfig) (state : IndeterminateProgressState) : Text

Render a progress bar for work with no known total. The filled segment bounces at both ends. The caller advances state.frame.

Equations

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

def TermColor.Widgets.defaultSpinnerFrames : List Text

Default braille spinner frames. The caller advances the frame index.

Equations

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

structure TermColor.Widgets.SpinnerState : Type

State displayed by a spinner. frame is selected modulo the configured frame count.

• frame : Nat
• label : Text

def TermColor.Widgets.instBEqSpinnerState.beq : SpinnerState → SpinnerState → Bool

Equations

• TermColor.Widgets.instBEqSpinnerState.beq { frame := a, label := a_1 } { frame := b, label := b_1 } = (a == b && a_1 == b_1)
• TermColor.Widgets.instBEqSpinnerState.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Widgets.instBEqSpinnerState : BEq SpinnerState

Equations

• TermColor.Widgets.instBEqSpinnerState = { beq := TermColor.Widgets.instBEqSpinnerState.beq }

def TermColor.Widgets.instDecidableEqSpinnerState.decEq (x✝ x✝¹ : SpinnerState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqSpinnerState : DecidableEq SpinnerState

Equations

• TermColor.Widgets.instDecidableEqSpinnerState = TermColor.Widgets.instDecidableEqSpinnerState.decEq

@[instance_reducible]

instance TermColor.Widgets.instReprSpinnerState : Repr SpinnerState

Equations

• TermColor.Widgets.instReprSpinnerState = { reprPrec := TermColor.Widgets.instReprSpinnerState.repr }

def TermColor.Widgets.instReprSpinnerState.repr : SpinnerState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedSpinnerState : Inhabited SpinnerState

Equations

• TermColor.Widgets.instInhabitedSpinnerState = { default := { } }

structure TermColor.Widgets.SpinnerConfig : Type

Rendering choices for a spinner. Empty frame lists render as an empty frame safely.

• frames : List Text
• prefixText : Text
• suffixText : Text

@[instance_reducible]

instance TermColor.Widgets.instBEqSpinnerConfig : BEq SpinnerConfig

Equations

• TermColor.Widgets.instBEqSpinnerConfig = { beq := TermColor.Widgets.instBEqSpinnerConfig.beq }

def TermColor.Widgets.instBEqSpinnerConfig.beq : SpinnerConfig → SpinnerConfig → Bool

Equations

• TermColor.Widgets.instBEqSpinnerConfig.beq { frames := a, prefixText := a_1, suffixText := a_2 } { frames := b, prefixText := b_1, suffixText := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• TermColor.Widgets.instBEqSpinnerConfig.beq x✝¹ x✝ = false

def TermColor.Widgets.instDecidableEqSpinnerConfig.decEq (x✝ x✝¹ : SpinnerConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqSpinnerConfig : DecidableEq SpinnerConfig

Equations

• TermColor.Widgets.instDecidableEqSpinnerConfig = TermColor.Widgets.instDecidableEqSpinnerConfig.decEq

def TermColor.Widgets.instReprSpinnerConfig.repr : SpinnerConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprSpinnerConfig : Repr SpinnerConfig

Equations

• TermColor.Widgets.instReprSpinnerConfig = { reprPrec := TermColor.Widgets.instReprSpinnerConfig.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedSpinnerConfig : Inhabited SpinnerConfig

Equations

• TermColor.Widgets.instInhabitedSpinnerConfig = { default := { } }

def TermColor.Widgets.spinnerFrame (config : SpinnerConfig) (frame : Nat) : Text

Select a spinner frame, wrapping around the configured frame list.

Equations

• TermColor.Widgets.spinnerFrame config frame = match config.frames with | [] => TermColor.Text.empty | frames => frames.getD (frame % frames.length) TermColor.Text.empty

def TermColor.Widgets.renderSpinner (config : SpinnerConfig) (state : SpinnerState) : Text

Render one spinner frame and its optional label as styled text.

Equations

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

structure TermColor.Widgets.ShimmerConfig : Type

Rendering choices for a moving brightness highlight. A zero phase step makes it breathe.

• base : Color
• highlight : Color
• band : Nat
• phaseStep : Nat

def TermColor.Widgets.instBEqShimmerConfig.beq : ShimmerConfig → ShimmerConfig → Bool

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instBEqShimmerConfig : BEq ShimmerConfig

Equations

• TermColor.Widgets.instBEqShimmerConfig = { beq := TermColor.Widgets.instBEqShimmerConfig.beq }

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqShimmerConfig : DecidableEq ShimmerConfig

Equations

• TermColor.Widgets.instDecidableEqShimmerConfig = TermColor.Widgets.instDecidableEqShimmerConfig.decEq

def TermColor.Widgets.instDecidableEqShimmerConfig.decEq (x✝ x✝¹ : ShimmerConfig) : Decidable (x✝ = x✝¹)

Equations

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

def TermColor.Widgets.instReprShimmerConfig.repr : ShimmerConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprShimmerConfig : Repr ShimmerConfig

Equations

• TermColor.Widgets.instReprShimmerConfig = { reprPrec := TermColor.Widgets.instReprShimmerConfig.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedShimmerConfig : Inhabited ShimmerConfig

Equations

• TermColor.Widgets.instInhabitedShimmerConfig = { default := { } }

structure TermColor.Widgets.ShimmerState : Type

State displayed by a shimmer. frame selects the current highlight phase.

• frame : Nat

@[instance_reducible]

instance TermColor.Widgets.instBEqShimmerState : BEq ShimmerState

Equations

• TermColor.Widgets.instBEqShimmerState = { beq := TermColor.Widgets.instBEqShimmerState.beq }

def TermColor.Widgets.instBEqShimmerState.beq : ShimmerState → ShimmerState → Bool

Equations

• TermColor.Widgets.instBEqShimmerState.beq { frame := a } { frame := b } = (a == b)
• TermColor.Widgets.instBEqShimmerState.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqShimmerState : DecidableEq ShimmerState

Equations

• TermColor.Widgets.instDecidableEqShimmerState = TermColor.Widgets.instDecidableEqShimmerState.decEq

def TermColor.Widgets.instDecidableEqShimmerState.decEq (x✝ x✝¹ : ShimmerState) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Widgets.instDecidableEqShimmerState.decEq { frame := a } { frame := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.Widgets.instReprShimmerState : Repr ShimmerState

Equations

• TermColor.Widgets.instReprShimmerState = { reprPrec := TermColor.Widgets.instReprShimmerState.repr }

def TermColor.Widgets.instReprShimmerState.repr : ShimmerState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedShimmerState : Inhabited ShimmerState

Equations

• TermColor.Widgets.instInhabitedShimmerState = { default := { } }

def TermColor.Widgets.shimmer (config : ShimmerConfig) (state : ShimmerState) (text : Text) : Text

Render a display-width-aware shimmer while preserving non-color text styles.

Equations

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

inductive TermColor.Widgets.StatusKind : Type

Common status markers for command-line messages.

• success : StatusKind
• info : StatusKind
• warning : StatusKind
• error : StatusKind

@[instance_reducible]

instance TermColor.Widgets.instBEqStatusKind : BEq StatusKind

Equations

• TermColor.Widgets.instBEqStatusKind = { beq := TermColor.Widgets.instBEqStatusKind.beq }

def TermColor.Widgets.instBEqStatusKind.beq : StatusKind → StatusKind → Bool

Equations

• TermColor.Widgets.instBEqStatusKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqStatusKind : DecidableEq StatusKind

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprStatusKind : Repr StatusKind

Equations

• TermColor.Widgets.instReprStatusKind = { reprPrec := TermColor.Widgets.instReprStatusKind.repr }

def TermColor.Widgets.instReprStatusKind.repr : StatusKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedStatusKind : Inhabited StatusKind

Equations

• TermColor.Widgets.instInhabitedStatusKind = { default := TermColor.Widgets.instInhabitedStatusKind.default }

def TermColor.Widgets.renderStatus (kind : StatusKind) (message : Text) : Text

Render a styled status marker followed by a message.

Equations

• TermColor.Widgets.renderStatus kind message = TermColor.Widgets.statusMarker✝ kind ++ TermColor.Text.plain " " ++ message

def TermColor.Widgets.renderTable (widths : List Nat) (rows : List (List Text)) (gap : Nat := 2) (alignments : List Layout.Alignment := []) : Text

Render rows as fixed-width, display-aware columns. Cells wrap to their column width.

Equations

• TermColor.Widgets.renderTable widths rows gap alignments = TermColor.Layout.joinLines (List.map (fun (row : List TermColor.Text) => TermColor.Layout.columns widths gap row alignments) rows)

inductive TermColor.Widgets.Key : Type

Keyboard input understood by pure interactive widgets.

• char (value : Char) : Key
• ctrl (value : Char) : Key
• left : Key
• right : Key
• home : Key
• end : Key
• up : Key
• down : Key
• pageUp : Key
• pageDown : Key
• enter : Key
• backspace : Key
• delete : Key
• tab : Key
• shiftTab : Key
• escape : Key

@[instance_reducible]

instance TermColor.Widgets.instBEqKey : BEq Key

Equations

• TermColor.Widgets.instBEqKey = { beq := TermColor.Widgets.instBEqKey.beq }

def TermColor.Widgets.instBEqKey.beq : Key → Key → Bool

Equations

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

def TermColor.Widgets.instDecidableEqKey.decEq (x✝ x✝¹ : Key) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqKey : DecidableEq Key

Equations

• TermColor.Widgets.instDecidableEqKey = TermColor.Widgets.instDecidableEqKey.decEq

@[instance_reducible]

instance TermColor.Widgets.instReprKey : Repr Key

Equations

• TermColor.Widgets.instReprKey = { reprPrec := TermColor.Widgets.instReprKey.repr }

def TermColor.Widgets.instReprKey.repr : Key → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Widgets.instReprKey.repr TermColor.Widgets.Key.end prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Widgets.Key.end")).group prec✝
• TermColor.Widgets.instReprKey.repr TermColor.Widgets.Key.up prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Widgets.Key.up")).group prec✝
• TermColor.Widgets.instReprKey.repr TermColor.Widgets.Key.tab prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Widgets.Key.tab")).group prec✝

structure TermColor.Widgets.CollapsibleKeyConfig : Type

Keyboard bindings for a collapsible widget. Focus traversal remains an application concern.

• toggleKeys : List Key
• expandKeys : List Key
• collapseKeys : List Key
• scrollUpKeys : List Key
• scrollDownKeys : List Key
• pageUpKeys : List Key
• pageDownKeys : List Key

@[instance_reducible]

instance TermColor.Widgets.instBEqCollapsibleKeyConfig : BEq CollapsibleKeyConfig

Equations

• TermColor.Widgets.instBEqCollapsibleKeyConfig = { beq := TermColor.Widgets.instBEqCollapsibleKeyConfig.beq }

def TermColor.Widgets.instBEqCollapsibleKeyConfig.beq : CollapsibleKeyConfig → CollapsibleKeyConfig → Bool

Equations

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

def TermColor.Widgets.instDecidableEqCollapsibleKeyConfig.decEq (x✝ x✝¹ : CollapsibleKeyConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqCollapsibleKeyConfig : DecidableEq CollapsibleKeyConfig

Equations

• TermColor.Widgets.instDecidableEqCollapsibleKeyConfig = TermColor.Widgets.instDecidableEqCollapsibleKeyConfig.decEq

def TermColor.Widgets.instReprCollapsibleKeyConfig.repr : CollapsibleKeyConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprCollapsibleKeyConfig : Repr CollapsibleKeyConfig

Equations

• TermColor.Widgets.instReprCollapsibleKeyConfig = { reprPrec := TermColor.Widgets.instReprCollapsibleKeyConfig.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedCollapsibleKeyConfig : Inhabited CollapsibleKeyConfig

Equations

• TermColor.Widgets.instInhabitedCollapsibleKeyConfig = { default := { } }

structure TermColor.Widgets.CollapsibleState : Type

Display state owned by one collapsible widget. The scroll offset counts wrapped body lines.

• expanded : Bool
• focused : Bool
• scrollOffset : Nat

def TermColor.Widgets.instBEqCollapsibleState.beq : CollapsibleState → CollapsibleState → Bool

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instBEqCollapsibleState : BEq CollapsibleState

Equations

• TermColor.Widgets.instBEqCollapsibleState = { beq := TermColor.Widgets.instBEqCollapsibleState.beq }

def TermColor.Widgets.instDecidableEqCollapsibleState.decEq (x✝ x✝¹ : CollapsibleState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqCollapsibleState : DecidableEq CollapsibleState

Equations

• TermColor.Widgets.instDecidableEqCollapsibleState = TermColor.Widgets.instDecidableEqCollapsibleState.decEq

def TermColor.Widgets.instReprCollapsibleState.repr : CollapsibleState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprCollapsibleState : Repr CollapsibleState

Equations

• TermColor.Widgets.instReprCollapsibleState = { reprPrec := TermColor.Widgets.instReprCollapsibleState.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedCollapsibleState : Inhabited CollapsibleState

Equations

• TermColor.Widgets.instInhabitedCollapsibleState = { default := { } }

structure TermColor.Widgets.CollapsibleConfig : Type

Rendering and keyboard choices for a collapsible widget.

• collapsedMarker : Text
• expandedMarker : Text
• summaryStyle : Style
• bodyStyle : Style
• focusStyle : Style
• bodyPrefix : Text
• maxBodyLines : Nat
• overflowText : Text
• emptyText : Text
• keys : CollapsibleKeyConfig

@[instance_reducible]

instance TermColor.Widgets.instBEqCollapsibleConfig : BEq CollapsibleConfig

Equations

• TermColor.Widgets.instBEqCollapsibleConfig = { beq := TermColor.Widgets.instBEqCollapsibleConfig.beq }

def TermColor.Widgets.instBEqCollapsibleConfig.beq : CollapsibleConfig → CollapsibleConfig → Bool

Equations

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

def TermColor.Widgets.instDecidableEqCollapsibleConfig.decEq (x✝ x✝¹ : CollapsibleConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqCollapsibleConfig : DecidableEq CollapsibleConfig

Equations

• TermColor.Widgets.instDecidableEqCollapsibleConfig = TermColor.Widgets.instDecidableEqCollapsibleConfig.decEq

@[instance_reducible]

instance TermColor.Widgets.instReprCollapsibleConfig : Repr CollapsibleConfig

Equations

• TermColor.Widgets.instReprCollapsibleConfig = { reprPrec := TermColor.Widgets.instReprCollapsibleConfig.repr }

def TermColor.Widgets.instReprCollapsibleConfig.repr : CollapsibleConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedCollapsibleConfig : Inhabited CollapsibleConfig

Equations

• TermColor.Widgets.instInhabitedCollapsibleConfig = { default := { } }

structure TermColor.Widgets.CollapsibleRender : Type

The rendered frame and geometry of a collapsible widget.

• text : Text
• lineCount : Nat
• hitHeaderHeight : Nat

@[instance_reducible]

instance TermColor.Widgets.instBEqCollapsibleRender : BEq CollapsibleRender

Equations

• TermColor.Widgets.instBEqCollapsibleRender = { beq := TermColor.Widgets.instBEqCollapsibleRender.beq }

def TermColor.Widgets.instBEqCollapsibleRender.beq : CollapsibleRender → CollapsibleRender → Bool

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqCollapsibleRender : DecidableEq CollapsibleRender

Equations

• TermColor.Widgets.instDecidableEqCollapsibleRender = TermColor.Widgets.instDecidableEqCollapsibleRender.decEq

def TermColor.Widgets.instDecidableEqCollapsibleRender.decEq (x✝ x✝¹ : CollapsibleRender) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprCollapsibleRender : Repr CollapsibleRender

Equations

• TermColor.Widgets.instReprCollapsibleRender = { reprPrec := TermColor.Widgets.instReprCollapsibleRender.repr }

def TermColor.Widgets.instReprCollapsibleRender.repr : CollapsibleRender → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedCollapsibleRender : Inhabited CollapsibleRender

Equations

• TermColor.Widgets.instInhabitedCollapsibleRender = { default := { text := TermColor.Text.empty, lineCount := 0, hitHeaderHeight := 0 } }

def TermColor.Widgets.toggleCollapsible (config : CollapsibleConfig) (width : Nat) (body : Text) (state : CollapsibleState) : CollapsibleState

Toggle expansion and, when opening, move to the newest buffered body lines.

Equations

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

def TermColor.Widgets.expandCollapsible (config : CollapsibleConfig) (width : Nat) (body : Text) (state : CollapsibleState) : CollapsibleState

Expand a collapsible and show its newest buffered body lines.

Equations

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

def TermColor.Widgets.collapseCollapsible (state : CollapsibleState) : CollapsibleState

Collapse a collapsible without changing its focus or scroll position.

Equations

• TermColor.Widgets.collapseCollapsible state = { focused := state.focused, scrollOffset := state.scrollOffset }

def TermColor.Widgets.scrollCollapsibleUp (config : CollapsibleConfig) (width : Nat) (body : Text) (state : CollapsibleState) : CollapsibleState

Scroll an expanded body toward its first line.

Equations

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

def TermColor.Widgets.scrollCollapsibleDown (config : CollapsibleConfig) (width : Nat) (body : Text) (state : CollapsibleState) : CollapsibleState

Scroll an expanded body toward its last line.

Equations

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

def TermColor.Widgets.pageUpCollapsible (config : CollapsibleConfig) (width : Nat) (body : Text) (state : CollapsibleState) : CollapsibleState

Scroll an expanded body one viewport toward its first line.

Equations

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

def TermColor.Widgets.pageDownCollapsible (config : CollapsibleConfig) (width : Nat) (body : Text) (state : CollapsibleState) : CollapsibleState

Scroll an expanded body one viewport toward its last line.

Equations

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

def TermColor.Widgets.handleCollapsibleKey (config : CollapsibleConfig) (width : Nat) (body : Text) (key : Key) (state : CollapsibleState) : CollapsibleState

Apply one configured key to a collapsible's pure display state.

Equations

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

def TermColor.Widgets.renderCollapsibleHeader (config : CollapsibleConfig) (width : Nat) (summary : Text) (state : CollapsibleState) : Text

Render the wrapped, focusable header of a collapsible widget.

Equations

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

def TermColor.Widgets.renderCollapsibleBody (config : CollapsibleConfig) (width : Nat) (body : Text) (state : CollapsibleState) : Text

Render the currently visible, wrapped body lines of an expanded widget.

Equations

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

def TermColor.Widgets.renderCollapsible (config : CollapsibleConfig) (width : Nat) (summary body : Text) (state : CollapsibleState) : CollapsibleRender

Render a collapsible with its visible line count and header hit height.

Equations

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

structure TermColor.Widgets.TextInputState : Type

State for a single-line text input. cursor is a code-point offset.

• value : String
• cursor : Nat

@[instance_reducible]

instance TermColor.Widgets.instBEqTextInputState : BEq TextInputState

Equations

• TermColor.Widgets.instBEqTextInputState = { beq := TermColor.Widgets.instBEqTextInputState.beq }

def TermColor.Widgets.instBEqTextInputState.beq : TextInputState → TextInputState → Bool

Equations

• TermColor.Widgets.instBEqTextInputState.beq { value := a, cursor := a_1 } { value := b, cursor := b_1 } = (a == b && a_1 == b_1)
• TermColor.Widgets.instBEqTextInputState.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqTextInputState : DecidableEq TextInputState

Equations

• TermColor.Widgets.instDecidableEqTextInputState = TermColor.Widgets.instDecidableEqTextInputState.decEq

def TermColor.Widgets.instDecidableEqTextInputState.decEq (x✝ x✝¹ : TextInputState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprTextInputState : Repr TextInputState

Equations

• TermColor.Widgets.instReprTextInputState = { reprPrec := TermColor.Widgets.instReprTextInputState.repr }

def TermColor.Widgets.instReprTextInputState.repr : TextInputState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedTextInputState : Inhabited TextInputState

Equations

• TermColor.Widgets.instInhabitedTextInputState = { default := { } }

structure TermColor.Widgets.TextInputConfig : Type

Rendering and input limits for a text input.

• width : Nat
• maxLength : Nat
• label : Text
• textStyle : Style
• cursorStyle : Style

def TermColor.Widgets.instBEqTextInputConfig.beq : TextInputConfig → TextInputConfig → Bool

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instBEqTextInputConfig : BEq TextInputConfig

Equations

• TermColor.Widgets.instBEqTextInputConfig = { beq := TermColor.Widgets.instBEqTextInputConfig.beq }

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqTextInputConfig : DecidableEq TextInputConfig

Equations

• TermColor.Widgets.instDecidableEqTextInputConfig = TermColor.Widgets.instDecidableEqTextInputConfig.decEq

def TermColor.Widgets.instDecidableEqTextInputConfig.decEq (x✝ x✝¹ : TextInputConfig) : Decidable (x✝ = x✝¹)

Equations

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

def TermColor.Widgets.instReprTextInputConfig.repr : TextInputConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprTextInputConfig : Repr TextInputConfig

Equations

• TermColor.Widgets.instReprTextInputConfig = { reprPrec := TermColor.Widgets.instReprTextInputConfig.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedTextInputConfig : Inhabited TextInputConfig

Equations

• TermColor.Widgets.instInhabitedTextInputConfig = { default := { } }

def TermColor.Widgets.updateTextInput (config : TextInputConfig) (key : Key) (state : TextInputState) : TextInputState

Apply one key to a text input. Input is limited by maxLength.

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Widgets.updateTextInput config TermColor.Widgets.Key.left state = { value := state.value, cursor := (TermColor.Widgets.clampCursor✝ state).pred }
• TermColor.Widgets.updateTextInput config TermColor.Widgets.Key.right state = { value := state.value, cursor := min state.value.toList.length (TermColor.Widgets.clampCursor✝ state + 1) }
• TermColor.Widgets.updateTextInput config TermColor.Widgets.Key.home state = { value := state.value }
• TermColor.Widgets.updateTextInput config (TermColor.Widgets.Key.ctrl 'a') state = { value := state.value }
• TermColor.Widgets.updateTextInput config TermColor.Widgets.Key.end state = { value := state.value, cursor := state.value.toList.length }
• TermColor.Widgets.updateTextInput config (TermColor.Widgets.Key.ctrl 'e') state = { value := state.value, cursor := state.value.toList.length }
• TermColor.Widgets.updateTextInput config (TermColor.Widgets.Key.ctrl 'u') state = { value := String.ofList (List.drop (TermColor.Widgets.clampCursor✝ state) state.value.toList) }
• TermColor.Widgets.updateTextInput config key state = { value := state.value, cursor := TermColor.Widgets.clampCursor✝ state }

def TermColor.Widgets.textInputBody (config : TextInputConfig) (state : TextInputState) (focused : Bool) : Text

Render the fixed-width input body without a frame, for embedding in a caller-owned layout.

Equations

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

def TermColor.Widgets.renderTextInput (config : TextInputConfig) (state : TextInputState) (focused : Bool := false) : Text

Render a single-line input with an optional visible cursor.

Equations

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

structure TermColor.Widgets.SliderState : Type

State for an integer slider. Values are clamped to the configured range.

• value : Nat

@[instance_reducible]

instance TermColor.Widgets.instBEqSliderState : BEq SliderState

Equations

• TermColor.Widgets.instBEqSliderState = { beq := TermColor.Widgets.instBEqSliderState.beq }

def TermColor.Widgets.instBEqSliderState.beq : SliderState → SliderState → Bool

Equations

• TermColor.Widgets.instBEqSliderState.beq { value := a } { value := b } = (a == b)
• TermColor.Widgets.instBEqSliderState.beq x✝¹ x✝ = false

def TermColor.Widgets.instDecidableEqSliderState.decEq (x✝ x✝¹ : SliderState) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Widgets.instDecidableEqSliderState.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqSliderState : DecidableEq SliderState

Equations

• TermColor.Widgets.instDecidableEqSliderState = TermColor.Widgets.instDecidableEqSliderState.decEq

def TermColor.Widgets.instReprSliderState.repr : SliderState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprSliderState : Repr SliderState

Equations

• TermColor.Widgets.instReprSliderState = { reprPrec := TermColor.Widgets.instReprSliderState.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedSliderState : Inhabited SliderState

Equations

• TermColor.Widgets.instInhabitedSliderState = { default := { } }

structure TermColor.Widgets.SliderConfig : Type

Rendering and movement choices for an integer slider.

• width : Nat
• min : Nat
• max : Nat
• step : Nat
• label : Text
• filledChar : Char
• emptyChar : Char
• filledStyle : Style
• emptyStyle : Style
• valueStyle : Style

@[instance_reducible]

instance TermColor.Widgets.instBEqSliderConfig : BEq SliderConfig

Equations

• TermColor.Widgets.instBEqSliderConfig = { beq := TermColor.Widgets.instBEqSliderConfig.beq }

def TermColor.Widgets.instBEqSliderConfig.beq : SliderConfig → SliderConfig → Bool

Equations

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

def TermColor.Widgets.instDecidableEqSliderConfig.decEq (x✝ x✝¹ : SliderConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqSliderConfig : DecidableEq SliderConfig

Equations

• TermColor.Widgets.instDecidableEqSliderConfig = TermColor.Widgets.instDecidableEqSliderConfig.decEq

def TermColor.Widgets.instReprSliderConfig.repr : SliderConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprSliderConfig : Repr SliderConfig

Equations

• TermColor.Widgets.instReprSliderConfig = { reprPrec := TermColor.Widgets.instReprSliderConfig.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedSliderConfig : Inhabited SliderConfig

Equations

• TermColor.Widgets.instInhabitedSliderConfig = { default := { } }

def TermColor.Widgets.sliderValue (config : SliderConfig) (state : SliderState) : Nat

Clamp a slider value, treating a reversed range as a single-value range.

Equations

• TermColor.Widgets.sliderValue config state = min (TermColor.Widgets.sliderMax✝ config) (max config.min state.value)

def TermColor.Widgets.updateSlider (config : SliderConfig) (key : Key) (state : SliderState) : SliderState

Apply one key to an integer slider.

Equations

• TermColor.Widgets.updateSlider config TermColor.Widgets.Key.left state = { value := TermColor.Widgets.sliderValue config state - config.step }
• TermColor.Widgets.updateSlider config TermColor.Widgets.Key.down state = { value := TermColor.Widgets.sliderValue config state - config.step }
• TermColor.Widgets.updateSlider config TermColor.Widgets.Key.right state = { value := min (TermColor.Widgets.sliderMax✝ config) (TermColor.Widgets.sliderValue config state + config.step) }
• TermColor.Widgets.updateSlider config TermColor.Widgets.Key.up state = { value := min (TermColor.Widgets.sliderMax✝ config) (TermColor.Widgets.sliderValue config state + config.step) }
• TermColor.Widgets.updateSlider config key state = { value := TermColor.Widgets.sliderValue config state }

def TermColor.Widgets.renderSlider (config : SliderConfig) (state : SliderState) : Text

Render an integer slider as a terminal bar and its current value.

Equations

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

structure TermColor.Widgets.CheckboxState : Type

State for a checkbox.

• checked : Bool

def TermColor.Widgets.instBEqCheckboxState.beq : CheckboxState → CheckboxState → Bool

Equations

• TermColor.Widgets.instBEqCheckboxState.beq { checked := a } { checked := b } = (a == b)
• TermColor.Widgets.instBEqCheckboxState.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Widgets.instBEqCheckboxState : BEq CheckboxState

Equations

• TermColor.Widgets.instBEqCheckboxState = { beq := TermColor.Widgets.instBEqCheckboxState.beq }

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqCheckboxState : DecidableEq CheckboxState

Equations

• TermColor.Widgets.instDecidableEqCheckboxState = TermColor.Widgets.instDecidableEqCheckboxState.decEq

def TermColor.Widgets.instDecidableEqCheckboxState.decEq (x✝ x✝¹ : CheckboxState) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Widgets.instDecidableEqCheckboxState.decEq { checked := a } { checked := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def TermColor.Widgets.instReprCheckboxState.repr : CheckboxState → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprCheckboxState : Repr CheckboxState

Equations

• TermColor.Widgets.instReprCheckboxState = { reprPrec := TermColor.Widgets.instReprCheckboxState.repr }

@[instance_reducible]

instance TermColor.Widgets.instInhabitedCheckboxState : Inhabited CheckboxState

Equations

• TermColor.Widgets.instInhabitedCheckboxState = { default := { } }

structure TermColor.Widgets.CheckboxConfig : Type

Rendering choices for a checkbox.

• label : Text
• checkedText : Text
• uncheckedText : Text

def TermColor.Widgets.instBEqCheckboxConfig.beq : CheckboxConfig → CheckboxConfig → Bool

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instBEqCheckboxConfig : BEq CheckboxConfig

Equations

• TermColor.Widgets.instBEqCheckboxConfig = { beq := TermColor.Widgets.instBEqCheckboxConfig.beq }

@[instance_reducible]

instance TermColor.Widgets.instDecidableEqCheckboxConfig : DecidableEq CheckboxConfig

Equations

• TermColor.Widgets.instDecidableEqCheckboxConfig = TermColor.Widgets.instDecidableEqCheckboxConfig.decEq

def TermColor.Widgets.instDecidableEqCheckboxConfig.decEq (x✝ x✝¹ : CheckboxConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instReprCheckboxConfig : Repr CheckboxConfig

Equations

• TermColor.Widgets.instReprCheckboxConfig = { reprPrec := TermColor.Widgets.instReprCheckboxConfig.repr }

def TermColor.Widgets.instReprCheckboxConfig.repr : CheckboxConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Widgets.instInhabitedCheckboxConfig : Inhabited CheckboxConfig

Equations

• TermColor.Widgets.instInhabitedCheckboxConfig = { default := { } }

def TermColor.Widgets.updateCheckbox (key : Key) (state : CheckboxState) : CheckboxState

Toggle a checkbox on activation.

Equations

• TermColor.Widgets.updateCheckbox (TermColor.Widgets.Key.char ' ') state = { checked := !state.checked }
• TermColor.Widgets.updateCheckbox TermColor.Widgets.Key.enter state = { checked := !state.checked }
• TermColor.Widgets.updateCheckbox key state = state

def TermColor.Widgets.renderCheckbox (config : CheckboxConfig) (state : CheckboxState) : Text

Render a checkbox with its label.

Equations

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

def TermColor.Widgets.buttonActivated : Key → Bool

Whether a key activates a button.

Equations

• TermColor.Widgets.buttonActivated TermColor.Widgets.Key.enter = true
• TermColor.Widgets.buttonActivated (TermColor.Widgets.Key.char ' ') = true
• TermColor.Widgets.buttonActivated x✝ = false

def TermColor.Widgets.renderButton (label : Text) (focused : Bool := false) : Text

Render a terminal button, highlighting it when focused.

Equations

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