TermColor.Terminal.Runtime

The smallest useful application runtime: typed resize/tick/input events, renderer injection, and terminal cleanup scoped with finally. Applications may use the lower-level pieces when they need a custom scheduler or background-job protocol.

structure TermColor.Terminal.Renderer (State : Type) : Type

A renderer owns its retained output state and terminal writes.

• start : IO State
• render : Size → State → Rendered → IO State
• finish : State → IO Unit

def TermColor.Terminal.lineRenderer (choice : ColorChoice := ColorChoice.auto) : Renderer Screen

Equations

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

def TermColor.Terminal.bufferRenderer (choice : ColorChoice := ColorChoice.auto) : Renderer BufferScreen

Equations

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

def TermColor.Terminal.withTerminal {α : Type} (action : IO α) : IO α

Scope cursor and alternate-screen state. Both controls restore on failure.

Equations

• TermColor.Terminal.withTerminal action = TermColor.Terminal.withHiddenCursor (TermColor.Terminal.withAlternateScreen action)

structure TermColor.Terminal.Cancellation : Type

• token : Std.CancellationToken

def TermColor.Terminal.Cancellation.new : IO Cancellation

Equations

• TermColor.Terminal.Cancellation.new = do let __do_lift ← liftM Std.CancellationToken.new pure { token := __do_lift }

def TermColor.Terminal.Cancellation.cancel (cancellation : Cancellation) : IO Unit

Equations

• cancellation.cancel = liftM cancellation.token.cancel

def TermColor.Terminal.Cancellation.isCancelled (cancellation : Cancellation) : IO Bool

Equations

• cancellation.isCancelled = liftM cancellation.token.isCancelled

inductive TermColor.Terminal.RuntimeEvent : Type

• input (event : Event) : RuntimeEvent
• resize (size : Size) : RuntimeEvent
• tick : RuntimeEvent

@[instance_reducible]

instance TermColor.Terminal.instBEqRuntimeEvent : BEq RuntimeEvent

Equations

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

def TermColor.Terminal.instBEqRuntimeEvent.beq : RuntimeEvent → RuntimeEvent → Bool

Equations

• TermColor.Terminal.instBEqRuntimeEvent.beq (TermColor.Terminal.RuntimeEvent.input a) (TermColor.Terminal.RuntimeEvent.input b) = (a == b)
• TermColor.Terminal.instBEqRuntimeEvent.beq (TermColor.Terminal.RuntimeEvent.resize a) (TermColor.Terminal.RuntimeEvent.resize b) = (a == b)
• TermColor.Terminal.instBEqRuntimeEvent.beq TermColor.Terminal.RuntimeEvent.tick TermColor.Terminal.RuntimeEvent.tick = true
• TermColor.Terminal.instBEqRuntimeEvent.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqRuntimeEvent : DecidableEq RuntimeEvent

Equations

• TermColor.Terminal.instDecidableEqRuntimeEvent = TermColor.Terminal.instDecidableEqRuntimeEvent.decEq

def TermColor.Terminal.instDecidableEqRuntimeEvent.decEq (x✝ x✝¹ : RuntimeEvent) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq (TermColor.Terminal.RuntimeEvent.input a) (TermColor.Terminal.RuntimeEvent.input b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq (TermColor.Terminal.RuntimeEvent.input event) (TermColor.Terminal.RuntimeEvent.resize size) = isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq (TermColor.Terminal.RuntimeEvent.input event) TermColor.Terminal.RuntimeEvent.tick = isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq (TermColor.Terminal.RuntimeEvent.resize size) (TermColor.Terminal.RuntimeEvent.input event) = isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq (TermColor.Terminal.RuntimeEvent.resize a) (TermColor.Terminal.RuntimeEvent.resize b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq (TermColor.Terminal.RuntimeEvent.resize size) TermColor.Terminal.RuntimeEvent.tick = isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq TermColor.Terminal.RuntimeEvent.tick (TermColor.Terminal.RuntimeEvent.input event) = isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq TermColor.Terminal.RuntimeEvent.tick (TermColor.Terminal.RuntimeEvent.resize size) = isFalse ⋯
• TermColor.Terminal.instDecidableEqRuntimeEvent.decEq TermColor.Terminal.RuntimeEvent.tick TermColor.Terminal.RuntimeEvent.tick = isTrue ⋯

def TermColor.Terminal.instReprRuntimeEvent.repr : RuntimeEvent → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprRuntimeEvent : Repr RuntimeEvent

Equations

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

structure TermColor.Terminal.EventReader : Type

• result : IO.Ref (Option (Option Event))
• active : IO.Ref Bool
• task : IO.Ref (Option (Task (Except IO.Error Unit)))

def TermColor.Terminal.EventReader.new : IO EventReader

Equations

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

def TermColor.Terminal.EventReader.ensureReading (reader : EventReader) (keepGoing : IO Bool) : IO Unit

Equations

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

def TermColor.Terminal.EventReader.take (reader : EventReader) : IO (Option (Option Event))

Equations

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

def TermColor.Terminal.EventReader.waitStopped (reader : EventReader) : IO Unit

Equations

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

structure TermColor.Terminal.LoopConfig (Model : Type) : Type

• initial : Model
• fallbackSize : Size
• tickMs : UInt32
• view : ViewContext → Model → Rendered
• update : RuntimeEvent → Model → Model
• isRunning : Model → Bool
• mouse : Bool

def TermColor.Terminal.run {Model State : Type} (renderer : Renderer State) (config : LoopConfig Model) : IO Unit

Run a small model/view loop with injectable renderer and guaranteed terminal cleanup.

Equations

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