TermColor.Terminal.Input

Pure decoding plus the small raw-input boundary used by interactive TUI applications.

inductive TermColor.Terminal.MouseButton : Type

• left : MouseButton
• middle : MouseButton
• right : MouseButton
• none : MouseButton
• other (value : Nat) : MouseButton

def TermColor.Terminal.instBEqMouseButton.beq : MouseButton → MouseButton → Bool

Equations

• TermColor.Terminal.instBEqMouseButton.beq TermColor.Terminal.MouseButton.left TermColor.Terminal.MouseButton.left = true
• TermColor.Terminal.instBEqMouseButton.beq TermColor.Terminal.MouseButton.middle TermColor.Terminal.MouseButton.middle = true
• TermColor.Terminal.instBEqMouseButton.beq TermColor.Terminal.MouseButton.right TermColor.Terminal.MouseButton.right = true
• TermColor.Terminal.instBEqMouseButton.beq TermColor.Terminal.MouseButton.none TermColor.Terminal.MouseButton.none = true
• TermColor.Terminal.instBEqMouseButton.beq (TermColor.Terminal.MouseButton.other a) (TermColor.Terminal.MouseButton.other b) = (a == b)
• TermColor.Terminal.instBEqMouseButton.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instBEqMouseButton : BEq MouseButton

Equations

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

def TermColor.Terminal.instDecidableEqMouseButton.decEq (x✝ x✝¹ : MouseButton) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.left TermColor.Terminal.MouseButton.left = isTrue ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.left (TermColor.Terminal.MouseButton.other value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.middle TermColor.Terminal.MouseButton.middle = isTrue ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.middle (TermColor.Terminal.MouseButton.other value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.right TermColor.Terminal.MouseButton.right = isTrue ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.right (TermColor.Terminal.MouseButton.other value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.none TermColor.Terminal.MouseButton.none = isTrue ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq TermColor.Terminal.MouseButton.none (TermColor.Terminal.MouseButton.other value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq (TermColor.Terminal.MouseButton.other value) TermColor.Terminal.MouseButton.left = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq (TermColor.Terminal.MouseButton.other value) TermColor.Terminal.MouseButton.middle = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq (TermColor.Terminal.MouseButton.other value) TermColor.Terminal.MouseButton.right = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq (TermColor.Terminal.MouseButton.other value) TermColor.Terminal.MouseButton.none = isFalse ⋯
• TermColor.Terminal.instDecidableEqMouseButton.decEq (TermColor.Terminal.MouseButton.other a) (TermColor.Terminal.MouseButton.other b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqMouseButton : DecidableEq MouseButton

Equations

• TermColor.Terminal.instDecidableEqMouseButton = TermColor.Terminal.instDecidableEqMouseButton.decEq

@[instance_reducible]

instance TermColor.Terminal.instReprMouseButton : Repr MouseButton

Equations

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

def TermColor.Terminal.instReprMouseButton.repr : MouseButton → Nat → Std.Format

Equations

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

inductive TermColor.Terminal.MouseAction : Type

• press : MouseAction
• release : MouseAction
• drag : MouseAction
• scrollUp : MouseAction
• scrollDown : MouseAction

@[instance_reducible]

instance TermColor.Terminal.instBEqMouseAction : BEq MouseAction

Equations

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

def TermColor.Terminal.instBEqMouseAction.beq : MouseAction → MouseAction → Bool

Equations

• TermColor.Terminal.instBEqMouseAction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqMouseAction : DecidableEq MouseAction

Equations

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

def TermColor.Terminal.instReprMouseAction.repr : MouseAction → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprMouseAction : Repr MouseAction

Equations

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

structure TermColor.Terminal.MouseModifiers : Type

• shift : Bool
• ctrl : Bool
• alt : Bool

@[instance_reducible]

instance TermColor.Terminal.instBEqMouseModifiers : BEq MouseModifiers

Equations

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

def TermColor.Terminal.instBEqMouseModifiers.beq : MouseModifiers → MouseModifiers → Bool

Equations

• TermColor.Terminal.instBEqMouseModifiers.beq { shift := a, ctrl := a_1, alt := a_2 } { shift := b, ctrl := b_1, alt := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• TermColor.Terminal.instBEqMouseModifiers.beq x✝¹ x✝ = false

def TermColor.Terminal.instDecidableEqMouseModifiers.decEq (x✝ x✝¹ : MouseModifiers) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqMouseModifiers : DecidableEq MouseModifiers

Equations

• TermColor.Terminal.instDecidableEqMouseModifiers = TermColor.Terminal.instDecidableEqMouseModifiers.decEq

@[instance_reducible]

instance TermColor.Terminal.instReprMouseModifiers : Repr MouseModifiers

Equations

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

def TermColor.Terminal.instReprMouseModifiers.repr : MouseModifiers → Nat → Std.Format

Equations

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

structure TermColor.Terminal.MouseEvent : Type

• button : MouseButton
• action : MouseAction
• column : Nat
• row : Nat
• modifiers : MouseModifiers

@[instance_reducible]

instance TermColor.Terminal.instBEqMouseEvent : BEq MouseEvent

Equations

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

def TermColor.Terminal.instBEqMouseEvent.beq : MouseEvent → MouseEvent → Bool

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqMouseEvent : DecidableEq MouseEvent

Equations

• TermColor.Terminal.instDecidableEqMouseEvent = TermColor.Terminal.instDecidableEqMouseEvent.decEq

def TermColor.Terminal.instDecidableEqMouseEvent.decEq (x✝ x✝¹ : MouseEvent) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprMouseEvent : Repr MouseEvent

Equations

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

def TermColor.Terminal.instReprMouseEvent.repr : MouseEvent → Nat → Std.Format

Equations

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

inductive TermColor.Terminal.Event : Type

• key (value : Widgets.Key) : Event
• mouse (value : MouseEvent) : Event

def TermColor.Terminal.instBEqEvent.beq : Event → Event → Bool

Equations

• TermColor.Terminal.instBEqEvent.beq (TermColor.Terminal.Event.key a) (TermColor.Terminal.Event.key b) = (a == b)
• TermColor.Terminal.instBEqEvent.beq (TermColor.Terminal.Event.mouse a) (TermColor.Terminal.Event.mouse b) = (a == b)
• TermColor.Terminal.instBEqEvent.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instBEqEvent : BEq Event

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqEvent : DecidableEq Event

Equations

• TermColor.Terminal.instDecidableEqEvent = TermColor.Terminal.instDecidableEqEvent.decEq

def TermColor.Terminal.instDecidableEqEvent.decEq (x✝ x✝¹ : Event) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqEvent.decEq (TermColor.Terminal.Event.key a) (TermColor.Terminal.Event.key b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.Terminal.instDecidableEqEvent.decEq (TermColor.Terminal.Event.key value) (TermColor.Terminal.Event.mouse value_1) = isFalse ⋯
• TermColor.Terminal.instDecidableEqEvent.decEq (TermColor.Terminal.Event.mouse value) (TermColor.Terminal.Event.key value_1) = isFalse ⋯
• TermColor.Terminal.instDecidableEqEvent.decEq (TermColor.Terminal.Event.mouse a) (TermColor.Terminal.Event.mouse b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def TermColor.Terminal.instReprEvent.repr : Event → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprEvent : Repr Event

Equations

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

inductive TermColor.Terminal.ByteRead : Type

One byte-level input result, including the raw terminal's timeout boundary.

• byte (value : UInt8) : ByteRead
• timeout : ByteRead
• eof : ByteRead

def TermColor.Terminal.instBEqByteRead.beq : ByteRead → ByteRead → Bool

Equations

• TermColor.Terminal.instBEqByteRead.beq (TermColor.Terminal.ByteRead.byte a) (TermColor.Terminal.ByteRead.byte b) = (a == b)
• TermColor.Terminal.instBEqByteRead.beq TermColor.Terminal.ByteRead.timeout TermColor.Terminal.ByteRead.timeout = true
• TermColor.Terminal.instBEqByteRead.beq TermColor.Terminal.ByteRead.eof TermColor.Terminal.ByteRead.eof = true
• TermColor.Terminal.instBEqByteRead.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Terminal.instBEqByteRead : BEq ByteRead

Equations

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

def TermColor.Terminal.instDecidableEqByteRead.decEq (x✝ x✝¹ : ByteRead) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqByteRead.decEq (TermColor.Terminal.ByteRead.byte a) (TermColor.Terminal.ByteRead.byte b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.Terminal.instDecidableEqByteRead.decEq (TermColor.Terminal.ByteRead.byte value) TermColor.Terminal.ByteRead.timeout = isFalse ⋯
• TermColor.Terminal.instDecidableEqByteRead.decEq (TermColor.Terminal.ByteRead.byte value) TermColor.Terminal.ByteRead.eof = isFalse ⋯
• TermColor.Terminal.instDecidableEqByteRead.decEq TermColor.Terminal.ByteRead.timeout (TermColor.Terminal.ByteRead.byte value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqByteRead.decEq TermColor.Terminal.ByteRead.timeout TermColor.Terminal.ByteRead.timeout = isTrue ⋯
• TermColor.Terminal.instDecidableEqByteRead.decEq TermColor.Terminal.ByteRead.timeout TermColor.Terminal.ByteRead.eof = isFalse TermColor.Terminal.instDecidableEqByteRead.decEq._proof_6
• TermColor.Terminal.instDecidableEqByteRead.decEq TermColor.Terminal.ByteRead.eof (TermColor.Terminal.ByteRead.byte value) = isFalse ⋯
• TermColor.Terminal.instDecidableEqByteRead.decEq TermColor.Terminal.ByteRead.eof TermColor.Terminal.ByteRead.timeout = isFalse TermColor.Terminal.instDecidableEqByteRead.decEq._proof_8
• TermColor.Terminal.instDecidableEqByteRead.decEq TermColor.Terminal.ByteRead.eof TermColor.Terminal.ByteRead.eof = isTrue ⋯

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqByteRead : DecidableEq ByteRead

Equations

• TermColor.Terminal.instDecidableEqByteRead = TermColor.Terminal.instDecidableEqByteRead.decEq

def TermColor.Terminal.instReprByteRead.repr : ByteRead → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprByteRead : Repr ByteRead

Equations

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

@[reducible, inline]

abbrev TermColor.Terminal.ByteSource : Type

An effectful byte source suitable for terminal input adapters.

Equations

• TermColor.Terminal.ByteSource = IO TermColor.Terminal.ByteRead

def TermColor.Terminal.parseKey (input : String) : Option Widgets.Key

Decode one complete terminal key sequence.

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Terminal.parseKey "\x1b[A" = some TermColor.Widgets.Key.up
• TermColor.Terminal.parseKey "\x1b[B" = some TermColor.Widgets.Key.down
• TermColor.Terminal.parseKey "\x1b[C" = some TermColor.Widgets.Key.right
• TermColor.Terminal.parseKey "\x1b[D" = some TermColor.Widgets.Key.left
• TermColor.Terminal.parseKey "\x1b[H" = some TermColor.Widgets.Key.home
• TermColor.Terminal.parseKey "\x1b[1~" = some TermColor.Widgets.Key.home
• TermColor.Terminal.parseKey "\x1b[F" = some TermColor.Widgets.Key.end
• TermColor.Terminal.parseKey "\x1b[4~" = some TermColor.Widgets.Key.end
• TermColor.Terminal.parseKey "\x1b[5~" = some TermColor.Widgets.Key.pageUp
• TermColor.Terminal.parseKey "\x1b[6~" = some TermColor.Widgets.Key.pageDown
• TermColor.Terminal.parseKey "\x1b[Z" = some TermColor.Widgets.Key.shiftTab
• TermColor.Terminal.parseKey "\x1b[1;2A" = some TermColor.Widgets.Key.up
• TermColor.Terminal.parseKey "\x1b[1;5A" = some TermColor.Widgets.Key.up
• TermColor.Terminal.parseKey "\x1b[1;2B" = some TermColor.Widgets.Key.down
• TermColor.Terminal.parseKey "\x1b[1;5B" = some TermColor.Widgets.Key.down
• TermColor.Terminal.parseKey "\x1b[1;2C" = some TermColor.Widgets.Key.right
• TermColor.Terminal.parseKey "\x1b[1;5C" = some TermColor.Widgets.Key.right
• TermColor.Terminal.parseKey "\x1b[1;2D" = some TermColor.Widgets.Key.left
• TermColor.Terminal.parseKey "\x1b[1;5D" = some TermColor.Widgets.Key.left
• TermColor.Terminal.parseKey "\x0d" = some TermColor.Widgets.Key.enter
• TermColor.Terminal.parseKey "\n" = some TermColor.Widgets.Key.enter
• TermColor.Terminal.parseKey "\x08" = some TermColor.Widgets.Key.backspace
• TermColor.Terminal.parseKey "\x7f" = some TermColor.Widgets.Key.backspace
• TermColor.Terminal.parseKey "\t" = some TermColor.Widgets.Key.tab
• TermColor.Terminal.parseKey "\x1b" = some TermColor.Widgets.Key.escape

def TermColor.Terminal.parseMouseEvent (input : String) : Option MouseEvent

Decode an SGR (1006) mouse sequence. Coordinates are one-based, like the protocol.

Equations

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

def TermColor.Terminal.parseEvent (input : String) : Option Event

Decode either a complete key sequence or a complete SGR mouse event.

Equations

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

def TermColor.Terminal.hitTest (frame : Frame) (event : MouseEvent) : Option String

Return the first hit region for a left-button press; releases and wheels are ignored.

Equations

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

def TermColor.Terminal.Screen.hitTest (screen : Screen) (event : MouseEvent) : Option String

Hit-test a mouse event against the frame currently owned by a screen.

Equations

• screen.hitTest event = TermColor.Terminal.hitTest screen.frame event

def TermColor.Terminal.moveFocus (count current : Nat) (key : Widgets.Key) : Nat

Move through an ordered set of focus slots, wrapping at either end.

Equations

• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.tab = if (count == 0) = true then 0 else (current + 1) % count
• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.down = if (count == 0) = true then 0 else (current + 1) % count
• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.right = if (count == 0) = true then 0 else (current + 1) % count
• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.pageDown = if (count == 0) = true then 0 else (current + 1) % count
• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.shiftTab = if (count == 0) = true then 0 else (current + count - 1) % count
• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.up = if (count == 0) = true then 0 else (current + count - 1) % count
• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.left = if (count == 0) = true then 0 else (current + count - 1) % count
• TermColor.Terminal.moveFocus count current TermColor.Widgets.Key.pageUp = if (count == 0) = true then 0 else (current + count - 1) % count
• TermColor.Terminal.moveFocus count current key = if (count == 0) = true then 0 else min current (count - 1)

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

Run an action with character-at-a-time terminal input, restoring the prior mode afterward.

Equations

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

partial def TermColor.Terminal.readEventFrom {m : Type → Type} [Monad m] (readByte : m ByteRead) (keepGoing : m Bool) : m (Option Event)

Decode one event from an injectable byte source.

def TermColor.Terminal.readEventWhile (keepGoing : IO Bool) : IO (Option Event)

Read one complete terminal event while a caller-owned condition holds.

Equations

• TermColor.Terminal.readEventWhile keepGoing = TermColor.Terminal.readEventFrom TermColor.Terminal.readByte✝ keepGoing

def TermColor.Terminal.readEvent : IO (Option Event)

Read one complete key or mouse event, waiting through raw-input timeouts.

Equations

• TermColor.Terminal.readEvent = TermColor.Terminal.readEventWhile (pure true)

def TermColor.Terminal.readKey : IO (Option Widgets.Key)

Read one ASCII terminal key, including the common arrow-key escape sequences.

Equations

• TermColor.Terminal.readKey = do let __do_lift ← TermColor.Terminal.readEvent match __do_lift with | some (TermColor.Terminal.Event.key key) => pure (some key) | x => pure none