TermColor.Repl.Terminal

Small terminal primitives shared by REPL loops. Model state, rendering, and submission remain callbacks supplied by the application.

structure TermColor.Repl.Terminal.Cancellation : Type

• token : Std.CancellationToken

def TermColor.Repl.Terminal.Cancellation.new : IO Cancellation

Equations

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

def TermColor.Repl.Terminal.Cancellation.cancel (token : Cancellation) : IO Unit

Equations

• token.cancel = liftM token.token.cancel

def TermColor.Repl.Terminal.Cancellation.isCancelled (token : Cancellation) : IO Bool

Equations

• token.isCancelled = liftM token.token.isCancelled

def TermColor.Repl.Terminal.Cancellation.sleep (token : Cancellation) (milliseconds : UInt32) : IO Bool

Equations

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

structure TermColor.Repl.Terminal.KeyReader : Type

• result : IO.Ref (Option (Option Widgets.Key))
• active : IO.Ref Bool
• signal : Std.Notify

def TermColor.Repl.Terminal.KeyReader.new : IO KeyReader

Equations

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

def TermColor.Repl.Terminal.KeyReader.ensureReading (reader : KeyReader) : IO Unit

Equations

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

structure TermColor.Repl.Terminal.JobConfig (Model : Type) : Type

Configuration for cooperative background jobs.

Multiple submitted lines may run at the same time. The renderer remains the owner of Model and Screen; each worker returns only model state which is merged through finish when its result is drained.

• shouldRun : Model → String → Bool
• start : Model → String → Model
• run : Cancellation → Model → String → IO Model
• tick : Model → IO Model

  Poll shared background state and advance live job presentation.

• finish : Model → Model → Model
• cancel : Model → Model
• fail : Model → String → Model

Application keymaps

structure TermColor.Repl.Terminal.AppKeymap (Model : Type) : Type 1

• Action : Type
• keymap : Keymap self.Action
• contexts : Model → List KeyContext
• handle : Model → self.Action → Option Model

def TermColor.Repl.Terminal.defaultFallbackSize : Terminal.Size

Equations

• TermColor.Repl.Terminal.defaultFallbackSize = { columns := 80, rows := 24 }

def TermColor.Repl.Terminal.defaultTickMs : UInt32

Equations

• TermColor.Repl.Terminal.defaultTickMs = 60

structure TermColor.Repl.Terminal.Config (Model : Type) : Type 1

• initial : Model
• inputConfig : Widgets.TextInputConfig
• multiline : Option MultilineConfig
• fallbackSize : Terminal.Size
• tickMs : UInt32
• resizeMs : UInt32

  Deprecated compatibility field; resize checks now follow tickMs.

• editorKeymap : Option (Keymap EditorAction)
• mouse : Bool
• view : Model → Terminal.Size → Text
• complete : Model → Widgets.TextInputState → IO (List Completion)
• keymap : Option (AppKeymap Model)

  Declarative application bindings. The first matching binding wins.

• handleKey : Model → Widgets.Key → Option Model

  Handle an application-specific key before the REPL edits its input.

• handleMouse : Model → Terminal.Size → Terminal.MouseEvent → Option Model

  Handle an application mouse event before the REPL ignores it.

• getState : Model → State
• setState : Model → State → Model
• submit : Model → String → IO Model
• jobs : Option (JobConfig Model)
• isRunning : Model → Bool
• quit : Model → Model

def TermColor.Repl.Terminal.currentSize (fallback : Terminal.Size) : IO Terminal.Size

Equations

• TermColor.Repl.Terminal.currentSize fallback = do let __do_lift ← TermColor.Terminal.terminalSize pure (__do_lift.getD fallback)

def TermColor.Repl.Terminal.readKeyWithResize (tickMs : UInt32) (fallback : Terminal.Size) (screen : Terminal.Screen) (render : Terminal.Screen → IO Terminal.Screen) (wake : IO Bool := pure false) (reader : Option KeyReader := none) (wakeSignal : Option Std.Notify := none) : IO (Terminal.Screen × Option Widgets.Key)

Equations

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

def TermColor.Repl.Terminal.run {Model : Type} (config : Config Model) : IO Unit

Equations

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

def TermColor.Repl.Terminal.suspend {α : Type} (action : IO α) : IO (Terminal.Screen × α)

Equations

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