TermColor.Terminal.UI

Small typed composition primitives for terminal applications. Views stay pure; the terminal runtime owns IO, while applications own model state and message handling.

structure TermColor.Terminal.Rect : Type

A one-based rectangle in terminal coordinates.

• top : Nat
• left : Nat
• width : Nat
• height : Nat

def TermColor.Terminal.instBEqRect.beq : Rect → Rect → Bool

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instBEqRect : BEq Rect

Equations

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

def TermColor.Terminal.instDecidableEqRect.decEq (x✝ x✝¹ : Rect) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqRect : DecidableEq Rect

Equations

• TermColor.Terminal.instDecidableEqRect = TermColor.Terminal.instDecidableEqRect.decEq

def TermColor.Terminal.instReprRect.repr : Rect → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprRect : Repr Rect

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedRect : Inhabited Rect

Equations

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

def TermColor.Terminal.Rect.right (rect : Rect) : Nat

Equations

• rect.right = rect.left + rect.width - 1

def TermColor.Terminal.Rect.bottom (rect : Rect) : Nat

Equations

• rect.bottom = rect.top + rect.height - 1

def TermColor.Terminal.Rect.move (rect : Rect) (top left : Nat) : Rect

Equations

• rect.move top left = { top := top, left := left, width := rect.width, height := rect.height }

def TermColor.Terminal.Rect.inset (rect : Rect) (rows columns : Nat) : Rect

Equations

• rect.inset rows columns = { top := rect.top + rows, left := rect.left + columns, width := rect.width - 2 * columns, height := rect.height - 2 * rows }

structure TermColor.Terminal.ViewContext : Type

Pure information supplied to every view.

• area : Rect
• size : Size

@[instance_reducible]

instance TermColor.Terminal.instBEqViewContext : BEq ViewContext

Equations

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

def TermColor.Terminal.instBEqViewContext.beq : ViewContext → ViewContext → Bool

Equations

• TermColor.Terminal.instBEqViewContext.beq { area := a, size := a_1 } { area := b, size := b_1 } = (a == b && a_1 == b_1)
• TermColor.Terminal.instBEqViewContext.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqViewContext : DecidableEq ViewContext

Equations

• TermColor.Terminal.instDecidableEqViewContext = TermColor.Terminal.instDecidableEqViewContext.decEq

def TermColor.Terminal.instDecidableEqViewContext.decEq (x✝ x✝¹ : ViewContext) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqViewContext.decEq { area := a, size := a_1 } { area := b, size := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.Terminal.instReprViewContext : Repr ViewContext

Equations

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

def TermColor.Terminal.instReprViewContext.repr : ViewContext → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedViewContext : Inhabited ViewContext

Equations

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

structure TermColor.Terminal.Rendered : Type

The pure result of rendering one component.

• text : Text
• hitRegions : List HitRegion
• focusables : List String
• focus : Option String

def TermColor.Terminal.instBEqRendered.beq : Rendered → Rendered → Bool

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instBEqRendered : BEq Rendered

Equations

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

def TermColor.Terminal.instDecidableEqRendered.decEq (x✝ x✝¹ : Rendered) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqRendered : DecidableEq Rendered

Equations

• TermColor.Terminal.instDecidableEqRendered = TermColor.Terminal.instDecidableEqRendered.decEq

def TermColor.Terminal.instReprRendered.repr : Rendered → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprRendered : Repr Rendered

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedRendered : Inhabited Rendered

Equations

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

def TermColor.Terminal.Rendered.width (rendered : Rendered) : Nat

Equations

• rendered.width = rendered.text.width

def TermColor.Terminal.Rendered.height (rendered : Rendered) : Nat

Equations

• rendered.height = rendered.text.height

def TermColor.Terminal.Rendered.toFrame (rendered : Rendered) : Frame

Equations

• rendered.toFrame = { text := rendered.text, hitRegions := rendered.hitRegions, focusables := rendered.focusables, focus := rendered.focus }

def TermColor.Terminal.Rendered.fromFrame (frame : Frame) : Rendered

Equations

• TermColor.Terminal.Rendered.fromFrame frame = { text := frame.text, hitRegions := frame.hitRegions, focusables := frame.focusables, focus := frame.focus }

def TermColor.Terminal.Rendered.withPrefix (name : String) (rendered : Rendered) : Rendered

Equations

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

def TermColor.Terminal.Rendered.vertical (gap : Nat) (items : List Rendered) : Rendered

Equations

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

def TermColor.Terminal.Rendered.horizontal (gap : Nat) (items : List Rendered) : Rendered

Equations

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

structure TermColor.Terminal.FocusRing : Type

Ordered focus state for a composed rendered tree.

• ids : List String
• current : Nat

@[instance_reducible]

instance TermColor.Terminal.instBEqFocusRing : BEq FocusRing

Equations

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

def TermColor.Terminal.instBEqFocusRing.beq : FocusRing → FocusRing → Bool

Equations

• TermColor.Terminal.instBEqFocusRing.beq { ids := a, current := a_1 } { ids := b, current := b_1 } = (a == b && a_1 == b_1)
• TermColor.Terminal.instBEqFocusRing.beq x✝¹ x✝ = false

def TermColor.Terminal.instDecidableEqFocusRing.decEq (x✝ x✝¹ : FocusRing) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqFocusRing.decEq { ids := a, current := a_1 } { ids := b, current := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqFocusRing : DecidableEq FocusRing

Equations

• TermColor.Terminal.instDecidableEqFocusRing = TermColor.Terminal.instDecidableEqFocusRing.decEq

def TermColor.Terminal.instReprFocusRing.repr : FocusRing → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprFocusRing : Repr FocusRing

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedFocusRing : Inhabited FocusRing

Equations

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

def TermColor.Terminal.FocusRing.fromRendered (rendered : Rendered) : FocusRing

Equations

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

def TermColor.Terminal.FocusRing.currentId (ring : FocusRing) : Option String

Equations

• ring.currentId = ring.ids[ring.current]?

def TermColor.Terminal.FocusRing.move (key : Widgets.Key) (ring : FocusRing) : FocusRing

Equations

• TermColor.Terminal.FocusRing.move key ring = { ids := ring.ids, current := TermColor.Terminal.moveFocus ring.ids.length ring.current key }

def TermColor.Terminal.FocusRing.focus (id : String) (ring : FocusRing) : FocusRing

Equations

• TermColor.Terminal.FocusRing.focus id ring = match TermColor.Terminal.FocusRing.indexOf?✝ id ring.ids with | some current => { ids := ring.ids, current := current } | none => ring

def TermColor.Terminal.target (rendered : Rendered) (ring : FocusRing) : Event → Option String

The component id receiving a terminal event after hit-testing/focus selection.

Equations

• TermColor.Terminal.target rendered ring (TermColor.Terminal.Event.key value) = ring.currentId
• TermColor.Terminal.target rendered ring (TermColor.Terminal.Event.mouse event) = TermColor.Terminal.hitTest rendered.toFrame event

inductive TermColor.Terminal.Constraint : Type

Width allocation used by row composition.

• fixed (width : Nat) : Constraint
• percent (value : Nat) : Constraint
• fill : Constraint

@[instance_reducible]

instance TermColor.Terminal.instBEqConstraint : BEq Constraint

Equations

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

def TermColor.Terminal.instBEqConstraint.beq : Constraint → Constraint → Bool

Equations

• TermColor.Terminal.instBEqConstraint.beq (TermColor.Terminal.Constraint.fixed a) (TermColor.Terminal.Constraint.fixed b) = (a == b)
• TermColor.Terminal.instBEqConstraint.beq (TermColor.Terminal.Constraint.percent a) (TermColor.Terminal.Constraint.percent b) = (a == b)
• TermColor.Terminal.instBEqConstraint.beq TermColor.Terminal.Constraint.fill TermColor.Terminal.Constraint.fill = true
• TermColor.Terminal.instBEqConstraint.beq x✝¹ x✝ = false

def TermColor.Terminal.instDecidableEqConstraint.decEq (x✝ x✝¹ : Constraint) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqConstraint.decEq (TermColor.Terminal.Constraint.fixed a) (TermColor.Terminal.Constraint.fixed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq (TermColor.Terminal.Constraint.fixed width) (TermColor.Terminal.Constraint.percent value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq (TermColor.Terminal.Constraint.fixed width) TermColor.Terminal.Constraint.fill = isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq (TermColor.Terminal.Constraint.percent value) (TermColor.Terminal.Constraint.fixed width) = isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq (TermColor.Terminal.Constraint.percent a) (TermColor.Terminal.Constraint.percent b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq (TermColor.Terminal.Constraint.percent value) TermColor.Terminal.Constraint.fill = isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq TermColor.Terminal.Constraint.fill (TermColor.Terminal.Constraint.fixed width) = isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq TermColor.Terminal.Constraint.fill (TermColor.Terminal.Constraint.percent value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqConstraint.decEq TermColor.Terminal.Constraint.fill TermColor.Terminal.Constraint.fill = isTrue ⋯

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqConstraint : DecidableEq Constraint

Equations

• TermColor.Terminal.instDecidableEqConstraint = TermColor.Terminal.instDecidableEqConstraint.decEq

@[instance_reducible]

instance TermColor.Terminal.instReprConstraint : Repr Constraint

Equations

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

def TermColor.Terminal.instReprConstraint.repr : Constraint → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedConstraint : Inhabited Constraint

Equations

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

def TermColor.Terminal.resolveConstraints (total gap : Nat) (constraints : List Constraint) : List Nat

Equations

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

structure TermColor.Terminal.View : Type

A pure view. The runtime decides how the resulting frame reaches the terminal.

• render : ViewContext → Rendered

def TermColor.Terminal.View.text (value : Text) : View

Equations

• TermColor.Terminal.View.text value = { render := fun (x : TermColor.Terminal.ViewContext) => { text := value } }

def TermColor.Terminal.View.frame (value : Frame) : View

Equations

• TermColor.Terminal.View.frame value = { render := fun (x : TermColor.Terminal.ViewContext) => TermColor.Terminal.Rendered.fromFrame value }

def TermColor.Terminal.View.column (gap : Nat) (children : List View) : View

Equations

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

def TermColor.Terminal.View.column.go (gap : Nat) (context : ViewContext) (offset : Nat) : List View → List Rendered

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Terminal.View.column.go gap context offset [] = []

def TermColor.Terminal.View.rowWith (constraints : List Constraint) (gap : Nat) (children : List View) : View

Equations

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

def TermColor.Terminal.View.rowWith.go (gap : Nat) (context : ViewContext) (offset : Nat) : List View → List Nat → List Rendered

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Terminal.View.rowWith.go gap context offset [] a✝ = []
• TermColor.Terminal.View.rowWith.go gap context offset a✝ [] = []

def TermColor.Terminal.View.row (gap : Nat) (children : List View) : View

Equations

• TermColor.Terminal.View.row gap children = TermColor.Terminal.View.rowWith (List.replicate children.length TermColor.Terminal.Constraint.fill) gap children

def TermColor.Terminal.View.panel (config : Layout.BoxConfig) (child : View) : View

Equations

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

def TermColor.Terminal.View.withPrefix (name : String) (child : View) : View

Equations

• TermColor.Terminal.View.withPrefix name child = { render := fun (context : TermColor.Terminal.ViewContext) => TermColor.Terminal.Rendered.withPrefix name (child.render context) }

inductive TermColor.Terminal.Command (Msg : Type) : Type

A command produced by a component update. Effects remain explicit and typed.

• none {Msg : Type} : Command Msg
• send {Msg : Type} (message : Msg) : Command Msg
• batch {Msg : Type} (commands : List (Command Msg)) : Command Msg
• task {Msg : Type} (work : IO Msg) : Command Msg

@[irreducible]

def TermColor.Terminal.Command.map {α β : Type} (convert : α → β) : Command α → Command β

Equations

• TermColor.Terminal.Command.map convert TermColor.Terminal.Command.none = TermColor.Terminal.Command.none
• TermColor.Terminal.Command.map convert (TermColor.Terminal.Command.send message) = TermColor.Terminal.Command.send (convert message)
• TermColor.Terminal.Command.map convert (TermColor.Terminal.Command.batch commands) = TermColor.Terminal.Command.batch (List.map (TermColor.Terminal.Command.map convert) commands)
• TermColor.Terminal.Command.map convert (TermColor.Terminal.Command.task work) = TermColor.Terminal.Command.task do let __do_lift ← work pure (convert __do_lift)

def TermColor.Terminal.Command.run {Msg : Type} (send : Msg → IO Unit) (command : Command Msg) : IO Unit

Execute a command tree with a caller-owned message sink.

Equations

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

structure TermColor.Terminal.Component (Model Msg : Type) : Type

Typed state/update/view contract for reusable application components.

• view : ViewContext → Model → Rendered
• update : Msg → Model → Model × List (Command Msg)

def TermColor.Terminal.Component.mapMsg {Model ChildMsg ParentMsg : Type} (inject : ChildMsg → ParentMsg) (project : ParentMsg → Option ChildMsg) (component : Component Model ChildMsg) : Component Model ParentMsg

Equations

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