TermColor.Terminal.Basic: terminal control and IO

The sequence builders are pure values. The IO helpers write to stdout and flush explicitly. Cursor controls are disabled for redirected output and TERM=dumb/TERM=unknown; live objects fall back to newline-separated snapshots in that mode. Live-region width follows the terminal on each default-width update; callers can pin it with updateTextAtWidth. Size detection is best effort: it queries /dev/tty for the current TTY size, then falls back to COLUMNS/LINES.

def TermColor.Terminal.cursorUpSequence (count : Nat) : String

Move the cursor up by count rows, or emit nothing for zero.

Equations

• TermColor.Terminal.cursorUpSequence count = if (count == 0) = true then "" else TermColor.Terminal.csi✝ ++ toString count ++ "A"

def TermColor.Terminal.cursorDownSequence (count : Nat) : String

Move the cursor down by count rows, or emit nothing for zero.

Equations

• TermColor.Terminal.cursorDownSequence count = if (count == 0) = true then "" else TermColor.Terminal.csi✝ ++ toString count ++ "B"

def TermColor.Terminal.cursorToColumnSequence (column : Nat) : String

Move to a one-based terminal column.

Equations

• TermColor.Terminal.cursorToColumnSequence column = TermColor.Terminal.csi✝ ++ toString (column + 1) ++ "G"

def TermColor.Terminal.clearLineSequence : String

Erase the current line and return to its first column.

Equations

• TermColor.Terminal.clearLineSequence = TermColor.Terminal.csi✝ ++ "2K\x0d"

def TermColor.Terminal.clearScreenSequence : String

Clear the visible screen and move the cursor to its home position.

Equations

• TermColor.Terminal.clearScreenSequence = TermColor.Terminal.csi✝ ++ "2J" ++ TermColor.Terminal.csi✝ ++ "H"

def TermColor.Terminal.saveCursorSequence : String

Save the current cursor position.

Equations

• TermColor.Terminal.saveCursorSequence = TermColor.Terminal.csi✝ ++ "s"

def TermColor.Terminal.restoreCursorSequence : String

Restore the previously saved cursor position.

Equations

• TermColor.Terminal.restoreCursorSequence = TermColor.Terminal.csi✝ ++ "u"

def TermColor.Terminal.enterAlternateScreenSequence : String

Enter the terminal's alternate screen buffer.

Equations

• TermColor.Terminal.enterAlternateScreenSequence = TermColor.Terminal.csi✝ ++ "?1049h"

def TermColor.Terminal.exitAlternateScreenSequence : String

Leave the terminal's alternate screen buffer.

Equations

• TermColor.Terminal.exitAlternateScreenSequence = TermColor.Terminal.csi✝ ++ "?1049l"

def TermColor.Terminal.hideCursorSequence : String

Hide the terminal cursor.

Equations

• TermColor.Terminal.hideCursorSequence = TermColor.Terminal.csi✝ ++ "?25l"

def TermColor.Terminal.showCursorSequence : String

Show the terminal cursor.

Equations

• TermColor.Terminal.showCursorSequence = TermColor.Terminal.csi✝ ++ "?25h"

def TermColor.Terminal.terminalControlAllowed (isTty : Bool) (term : Option String) : Bool

Whether a TTY and terminal declaration allow cursor-control sequences.

Equations

• TermColor.Terminal.terminalControlAllowed isTty (some "dumb") = if (!isTty) = true then false else false
• TermColor.Terminal.terminalControlAllowed isTty (some "unknown") = if (!isTty) = true then false else false
• TermColor.Terminal.terminalControlAllowed isTty term = if (!isTty) = true then false else true

def TermColor.Terminal.write (text : String) : IO Unit

Write text to stdout without flushing.

Equations

• TermColor.Terminal.write text = IO.print text

def TermColor.Terminal.flush : IO Unit

Flush stdout.

Equations

• TermColor.Terminal.flush = do let __do_lift ← liftM IO.getStdout __do_lift.flush

def TermColor.Terminal.writeText (text : Text) (choice : ColorChoice := ColorChoice.auto) : IO Unit

Render styled text using terminal detection and write it without a newline.

Equations

• TermColor.Terminal.writeText text choice = do let __do_lift ← TermColor.render text choice TermColor.Terminal.write __do_lift

def TermColor.Terminal.writeTextLine (text : Text) (choice : ColorChoice := ColorChoice.auto) : IO Unit

Render styled text using terminal detection and write it with a newline.

Equations

• TermColor.Terminal.writeTextLine text choice = do let __do_lift ← TermColor.render (text ++ TermColor.Text.plain "\n") choice TermColor.Terminal.write __do_lift

def TermColor.Terminal.clearLine : IO Unit

Erase the current line and return to its first column.

Equations

• TermColor.Terminal.clearLine = TermColor.Terminal.writeControl✝ TermColor.Terminal.clearLineSequence

def TermColor.Terminal.clearScreen : IO Unit

Clear the visible screen and flush stdout.

Equations

• TermColor.Terminal.clearScreen = TermColor.Terminal.writeControl✝ TermColor.Terminal.clearScreenSequence

def TermColor.Terminal.saveCursor : IO Unit

Save the cursor position and flush stdout.

Equations

• TermColor.Terminal.saveCursor = TermColor.Terminal.writeControl✝ TermColor.Terminal.saveCursorSequence

def TermColor.Terminal.restoreCursor : IO Unit

Restore the cursor position and flush stdout.

Equations

• TermColor.Terminal.restoreCursor = TermColor.Terminal.writeControl✝ TermColor.Terminal.restoreCursorSequence

def TermColor.Terminal.enterAlternateScreen : IO Unit

Enter the alternate screen buffer and flush stdout.

Equations

• TermColor.Terminal.enterAlternateScreen = TermColor.Terminal.writeControl✝ TermColor.Terminal.enterAlternateScreenSequence

def TermColor.Terminal.exitAlternateScreen : IO Unit

Leave the alternate screen buffer and flush stdout.

Equations

• TermColor.Terminal.exitAlternateScreen = TermColor.Terminal.writeControl✝ TermColor.Terminal.exitAlternateScreenSequence

def TermColor.Terminal.cursorUp (count : Nat) : IO Unit

Move the cursor up and flush stdout.

Equations

• TermColor.Terminal.cursorUp count = TermColor.Terminal.writeControl✝ (TermColor.Terminal.cursorUpSequence count)

def TermColor.Terminal.cursorDown (count : Nat) : IO Unit

Move the cursor down and flush stdout.

Equations

• TermColor.Terminal.cursorDown count = TermColor.Terminal.writeControl✝ (TermColor.Terminal.cursorDownSequence count)

def TermColor.Terminal.cursorToColumn (column : Nat) : IO Unit

Move to a one-based terminal column and flush stdout.

Equations

• TermColor.Terminal.cursorToColumn column = TermColor.Terminal.writeControl✝ (TermColor.Terminal.cursorToColumnSequence column)

def TermColor.Terminal.hideCursor : IO Unit

Hide the terminal cursor and flush stdout.

Equations

• TermColor.Terminal.hideCursor = TermColor.Terminal.writeControl✝ TermColor.Terminal.hideCursorSequence

def TermColor.Terminal.showCursor : IO Unit

Show the terminal cursor and flush stdout.

Equations

• TermColor.Terminal.showCursor = TermColor.Terminal.writeControl✝ TermColor.Terminal.showCursorSequence

def TermColor.Terminal.stdoutIsTty : IO Bool

Whether stdout is attached to a terminal.

Equations

• TermColor.Terminal.stdoutIsTty = do let __do_lift ← liftM IO.getStdout liftM __do_lift.isTty

def TermColor.Terminal.stdoutSupportsControl : IO Bool

Whether stdout is a TTY suitable for cursor-control sequences.

Equations

• TermColor.Terminal.stdoutSupportsControl = TermColor.Terminal.terminalControlEnabled✝

def TermColor.Terminal.stdinIsTty : IO Bool

Whether stdin is attached to a terminal.

Equations

• TermColor.Terminal.stdinIsTty = do let __do_lift ← liftM IO.getStdin liftM __do_lift.isTty

structure TermColor.Terminal.Size : Type

A terminal's usable character dimensions.

• columns : Nat
• rows : Nat

@[instance_reducible]

instance TermColor.Terminal.instBEqSize : BEq Size

Equations

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

def TermColor.Terminal.instBEqSize.beq : Size → Size → Bool

Equations

• TermColor.Terminal.instBEqSize.beq { columns := a, rows := a_1 } { columns := b, rows := b_1 } = (a == b && a_1 == b_1)
• TermColor.Terminal.instBEqSize.beq x✝¹ x✝ = false

def TermColor.Terminal.instDecidableEqSize.decEq (x✝ x✝¹ : Size) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Terminal.instDecidableEqSize.decEq { columns := a, rows := a_1 } { columns := b, rows := 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.instDecidableEqSize : DecidableEq Size

Equations

• TermColor.Terminal.instDecidableEqSize = TermColor.Terminal.instDecidableEqSize.decEq

def TermColor.Terminal.instReprSize.repr : Size → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprSize : Repr Size

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedSize : Inhabited Size

Equations

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

def TermColor.Terminal.parseSize (output : String) : Option Size

Parse the rows columns output convention used by stty size.

Equations

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

opaque TermColor.Terminal.terminalSizeCache : IO.Ref (Option (Nat × Option Size))

def TermColor.Terminal.terminalSize : IO (Option Size)

Query terminal dimensions, returning none when no size can be determined.

Equations

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

def TermColor.Terminal.terminalWidth : IO Nat

Query terminal width, falling back to the layout library's default width.

Equations

• TermColor.Terminal.terminalWidth = do let __do_lift ← TermColor.Terminal.terminalSize match __do_lift with | some size => pure size.columns | none => pure TermColor.Layout.defaultWidth

structure TermColor.Terminal.HitRegion : Type

A stable application-owned rectangle in one-based terminal coordinates.

• id : String
• top : Nat
• bottom : Nat
• left : Nat
• right : Nat

def TermColor.Terminal.instBEqHitRegion.beq : HitRegion → HitRegion → Bool

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instBEqHitRegion : BEq HitRegion

Equations

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

def TermColor.Terminal.instDecidableEqHitRegion.decEq (x✝ x✝¹ : HitRegion) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqHitRegion : DecidableEq HitRegion

Equations

• TermColor.Terminal.instDecidableEqHitRegion = TermColor.Terminal.instDecidableEqHitRegion.decEq

def TermColor.Terminal.instReprHitRegion.repr : HitRegion → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprHitRegion : Repr HitRegion

Equations

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

def TermColor.Terminal.HitRegion.contains (region : HitRegion) (row column : Nat) : Bool

Whether a one-based terminal coordinate lies inside a hit region.

Equations

• region.contains row column = (decide (region.top ≤ row) && decide (row ≤ region.bottom) && decide (region.left ≤ column) && decide (column ≤ region.right))

structure TermColor.Terminal.Frame : Type

A pure frame supplied to Screen.renderFrame.

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

@[instance_reducible]

instance TermColor.Terminal.instBEqFrame : BEq Frame

Equations

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

def TermColor.Terminal.instBEqFrame.beq : Frame → Frame → Bool

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instDecidableEqFrame : DecidableEq Frame

Equations

• TermColor.Terminal.instDecidableEqFrame = TermColor.Terminal.instDecidableEqFrame.decEq

def TermColor.Terminal.instDecidableEqFrame.decEq (x✝ x✝¹ : Frame) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instReprFrame : Repr Frame

Equations

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

def TermColor.Terminal.instReprFrame.repr : Frame → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Terminal.instInhabitedFrame : Inhabited Frame

Equations

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

structure TermColor.Terminal.Screen : Type

Retained line-oriented screen state for small full-screen applications.

• previous : List String
• size : Option TermColor.Terminal.Size
• frame : Frame

def TermColor.Terminal.Screen.empty : Screen

Empty screen state, useful when testing diffSequence without terminal IO.

Equations

• TermColor.Terminal.Screen.empty = { }

def TermColor.Terminal.Screen.start : IO Screen

Start a screen and capture the current terminal size.

Equations

• TermColor.Terminal.Screen.start = do let __do_lift ← TermColor.Terminal.terminalSize pure { size := __do_lift }

def TermColor.Terminal.Screen.diffSequence (screen : Screen) (next : List String) : String × Screen

Pure line-granularity diff from the previous screen to next.

Equations

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

def TermColor.Terminal.Screen.renderFrame (screen : Screen) (frame : Frame) (choice : ColorChoice := ColorChoice.auto) : IO Screen

Render a frame, atomically retaining its hit regions after the write succeeds.

Equations

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

def TermColor.Terminal.Screen.render (screen : Screen) (text : Text) (choice : ColorChoice := ColorChoice.auto) : IO Screen

Render a screen, rewriting only lines whose visible text changed.

Equations

• screen.render text choice = screen.renderFrame { text := text } choice

def TermColor.Terminal.Screen.finish (screen : Screen) : IO Screen

Finish a screen and leave the cursor below its last rendered line.

Equations

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

def TermColor.Terminal.mouseCaptureSequence (enabled drag : Bool) : String

Enable SGR mouse events, optionally including drag reporting.

Equations

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

def TermColor.Terminal.enableMouse (drag : Bool := false) : IO Unit

Enable mouse reporting when stdout is a capable terminal.

Equations

• TermColor.Terminal.enableMouse drag = TermColor.Terminal.writeControl✝ (TermColor.Terminal.mouseCaptureSequence true drag)

def TermColor.Terminal.disableMouse (drag : Bool := false) : IO Unit

Disable mouse reporting.

Equations

• TermColor.Terminal.disableMouse drag = TermColor.Terminal.writeControl✝ (TermColor.Terminal.mouseCaptureSequence false drag)

def TermColor.Terminal.withMouseCapture {α : Type} (action : IO α) (drag : Bool := false) : IO α

Scope mouse reporting and restore the terminal mode even when the action fails.

Equations

• TermColor.Terminal.withMouseCapture action drag = do TermColor.Terminal.enableMouse drag tryFinally action (TermColor.Terminal.disableMouse drag)

structure TermColor.Terminal.LiveRegion : Type

State for redrawing a multi-line terminal region in place.

• lineCount : Nat
• width : Option Nat

def TermColor.Terminal.LiveRegion.start : LiveRegion

Start an inactive live region.

Equations

• TermColor.Terminal.LiveRegion.start = { }

def TermColor.Terminal.LiveRegion.setWidth (state : LiveRegion) (width : Nat) : LiveRegion

Use a supplied width for subsequent text updates.

Equations

• state.setWidth width = { lineCount := state.lineCount, width := some width }

def TermColor.Terminal.LiveRegion.updateSequence (state : LiveRegion) (text : String) : String × LiveRegion

Pure output and next state for a multi-line redraw.

Equations

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

def TermColor.Terminal.LiveRegion.finishSequence (state : LiveRegion) : String × LiveRegion

Pure output and next state for finishing a live region.

Equations

• state.finishSequence = (if (state.lineCount == 0) = true then "" else "\n", { })

def TermColor.Terminal.LiveRegion.update (state : LiveRegion) (text : String) : IO LiveRegion

Redraw a multi-line region and flush stdout.

Equations

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

def TermColor.Terminal.LiveRegion.updateTextAtWidth (state : LiveRegion) (width : Nat) (text : Text) (choice : ColorChoice := ColorChoice.auto) : IO LiveRegion

Render styled text at a supplied width, redraw a multi-line region, and flush stdout.

Equations

• state.updateTextAtWidth width text choice = do let __do_lift ← TermColor.Terminal.LiveRegion.renderTextAtWidth✝ width text choice (state.setWidth width).update __do_lift

def TermColor.Terminal.LiveRegion.updateText (state : LiveRegion) (text : Text) (choice : ColorChoice := ColorChoice.auto) : IO LiveRegion

Render styled text at the current terminal width, redraw the region, and flush stdout.

When the region has no explicit width, the terminal is queried for every update so live output can reflow after a window resize.

Equations

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

def TermColor.Terminal.LiveRegion.finish (state : LiveRegion) : IO LiveRegion

Leave the live region in place and move to the next line.

Equations

• state.finish = match state.finishSequence with | (output, next) => do TermColor.Terminal.write output TermColor.Terminal.flush pure next

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

Hide the cursor for an action and restore it even when the action fails.

Equations

• TermColor.Terminal.withHiddenCursor action = do TermColor.Terminal.hideCursor tryFinally action TermColor.Terminal.showCursor

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

Run an action in the alternate screen buffer and restore the normal screen afterward.

Equations

• TermColor.Terminal.withAlternateScreen action = do TermColor.Terminal.enterAlternateScreen tryFinally action TermColor.Terminal.exitAlternateScreen