TermColor.Repl

Pure input history, key handling, and adaptive completion for terminal REPLs. The terminal loop is intentionally separate so applications can keep ownership of their model and transcript while reusing this state machine.

inductive TermColor.Repl.CompletionKind : Type

• text : CompletionKind
• file : CompletionKind
• directory : CompletionKind
• executable : CompletionKind

@[instance_reducible]

instance TermColor.Repl.instReprCompletionKind : Repr CompletionKind

Equations

• TermColor.Repl.instReprCompletionKind = { reprPrec := TermColor.Repl.instReprCompletionKind.repr }

def TermColor.Repl.instReprCompletionKind.repr : CompletionKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instBEqCompletionKind : BEq CompletionKind

Equations

• TermColor.Repl.instBEqCompletionKind = { beq := TermColor.Repl.instBEqCompletionKind.beq }

def TermColor.Repl.instBEqCompletionKind.beq : CompletionKind → CompletionKind → Bool

Equations

• TermColor.Repl.instBEqCompletionKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.Repl.instDecidableEqCompletionKind : DecidableEq CompletionKind

Equations

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

structure TermColor.Repl.Completion : Type

• replacement : String
• label : String
• kind : CompletionKind
• range : Option (Nat × Nat)

@[instance_reducible]

instance TermColor.Repl.instReprCompletion : Repr Completion

Equations

• TermColor.Repl.instReprCompletion = { reprPrec := TermColor.Repl.instReprCompletion.repr }

def TermColor.Repl.instReprCompletion.repr : Completion → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instBEqCompletion : BEq Completion

Equations

• TermColor.Repl.instBEqCompletion = { beq := TermColor.Repl.instBEqCompletion.beq }

def TermColor.Repl.instBEqCompletion.beq : Completion → Completion → Bool

Equations

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

def TermColor.Repl.instDecidableEqCompletion.decEq (x✝ x✝¹ : Completion) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Repl.instDecidableEqCompletion : DecidableEq Completion

Equations

• TermColor.Repl.instDecidableEqCompletion = TermColor.Repl.instDecidableEqCompletion.decEq

structure TermColor.Repl.CompletionMenu : Type

• candidates : Array Completion
• selected : Nat

def TermColor.Repl.instReprCompletionMenu.repr : CompletionMenu → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instReprCompletionMenu : Repr CompletionMenu

Equations

• TermColor.Repl.instReprCompletionMenu = { reprPrec := TermColor.Repl.instReprCompletionMenu.repr }

def TermColor.Repl.instBEqCompletionMenu.beq : CompletionMenu → CompletionMenu → Bool

Equations

• TermColor.Repl.instBEqCompletionMenu.beq { candidates := a, selected := a_1 } { candidates := b, selected := b_1 } = (a == b && a_1 == b_1)
• TermColor.Repl.instBEqCompletionMenu.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Repl.instBEqCompletionMenu : BEq CompletionMenu

Equations

• TermColor.Repl.instBEqCompletionMenu = { beq := TermColor.Repl.instBEqCompletionMenu.beq }

def TermColor.Repl.instDecidableEqCompletionMenu.decEq (x✝ x✝¹ : CompletionMenu) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Repl.instDecidableEqCompletionMenu : DecidableEq CompletionMenu

Equations

• TermColor.Repl.instDecidableEqCompletionMenu = TermColor.Repl.instDecidableEqCompletionMenu.decEq

structure TermColor.Repl.CompletionMenuConfig : Type

• width : Nat
• maxItems : Nat
• selectedStyle : Style
• textStyle : Style
• kindStyle : Style

@[instance_reducible]

instance TermColor.Repl.instReprCompletionMenuConfig : Repr CompletionMenuConfig

Equations

• TermColor.Repl.instReprCompletionMenuConfig = { reprPrec := TermColor.Repl.instReprCompletionMenuConfig.repr }

def TermColor.Repl.instReprCompletionMenuConfig.repr : CompletionMenuConfig → Nat → Std.Format

Equations

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

structure TermColor.Repl.State : Type

• input : Widgets.TextInputState
• history : Array String
• historyIndex : Option Nat
• completion : Option CompletionMenu

def TermColor.Repl.instReprState.repr : State → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instReprState : Repr State

Equations

• TermColor.Repl.instReprState = { reprPrec := TermColor.Repl.instReprState.repr }

structure TermColor.Repl.MultilineConfig : Type

• text : Widgets.TextInputConfig
• lineBreak : Widgets.Key
• keymap : Option (Keymap EditorAction)

def TermColor.Repl.instReprMultilineConfig.repr : MultilineConfig → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instReprMultilineConfig : Repr MultilineConfig

Equations

• TermColor.Repl.instReprMultilineConfig = { reprPrec := TermColor.Repl.instReprMultilineConfig.repr }

inductive TermColor.Repl.Action : Type

• changed : Action
• submit (line : String) : Action
• quit : Action

def TermColor.Repl.instReprAction.repr : Action → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instReprAction : Repr Action

Equations

• TermColor.Repl.instReprAction = { reprPrec := TermColor.Repl.instReprAction.repr }

def TermColor.Repl.instBEqAction.beq : Action → Action → Bool

Equations

• TermColor.Repl.instBEqAction.beq TermColor.Repl.Action.changed TermColor.Repl.Action.changed = true
• TermColor.Repl.instBEqAction.beq (TermColor.Repl.Action.submit a) (TermColor.Repl.Action.submit b) = (a == b)
• TermColor.Repl.instBEqAction.beq TermColor.Repl.Action.quit TermColor.Repl.Action.quit = true
• TermColor.Repl.instBEqAction.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.Repl.instBEqAction : BEq Action

Equations

• TermColor.Repl.instBEqAction = { beq := TermColor.Repl.instBEqAction.beq }

@[instance_reducible]

instance TermColor.Repl.instDecidableEqAction : DecidableEq Action

Equations

• TermColor.Repl.instDecidableEqAction = TermColor.Repl.instDecidableEqAction.decEq

def TermColor.Repl.instDecidableEqAction.decEq (x✝ x✝¹ : Action) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Repl.instDecidableEqAction.decEq TermColor.Repl.Action.changed TermColor.Repl.Action.changed = isTrue ⋯
• TermColor.Repl.instDecidableEqAction.decEq TermColor.Repl.Action.changed (TermColor.Repl.Action.submit line) = isFalse ⋯
• TermColor.Repl.instDecidableEqAction.decEq TermColor.Repl.Action.changed TermColor.Repl.Action.quit = isFalse TermColor.Repl.instDecidableEqAction.decEq._proof_2
• TermColor.Repl.instDecidableEqAction.decEq (TermColor.Repl.Action.submit line) TermColor.Repl.Action.changed = isFalse ⋯
• TermColor.Repl.instDecidableEqAction.decEq (TermColor.Repl.Action.submit a) (TermColor.Repl.Action.submit b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.Repl.instDecidableEqAction.decEq (TermColor.Repl.Action.submit line) TermColor.Repl.Action.quit = isFalse ⋯
• TermColor.Repl.instDecidableEqAction.decEq TermColor.Repl.Action.quit TermColor.Repl.Action.changed = isFalse TermColor.Repl.instDecidableEqAction.decEq._proof_7
• TermColor.Repl.instDecidableEqAction.decEq TermColor.Repl.Action.quit (TermColor.Repl.Action.submit line) = isFalse ⋯
• TermColor.Repl.instDecidableEqAction.decEq TermColor.Repl.Action.quit TermColor.Repl.Action.quit = isTrue ⋯

def TermColor.Repl.completeInput (input : Widgets.TextInputState) (candidates : List Completion) : Widgets.TextInputState

Equations

• One or more equations did not get rendered due to their size.
• TermColor.Repl.completeInput input [] = input
• TermColor.Repl.completeInput input [candidate] = TermColor.Repl.applyCompletion✝ input candidate

def TermColor.Repl.renderMultilineTextInputBody (config : Widgets.TextInputConfig) (state : Widgets.TextInputState) (focused : Bool := false) : Text

Equations

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

def TermColor.Repl.renderCompletionMenu (config : CompletionMenuConfig) (menu : CompletionMenu) : Text

Render a width-bounded completion menu with a selected row and kind markers.

Equations

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

def TermColor.Repl.recallUp (state : State) : State

Equations

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

def TermColor.Repl.recallDown (state : State) : State

Equations

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

def TermColor.Repl.updateMultilineWithKeymap (config : MultilineConfig) (keymap : Keymap EditorAction) (complete : Widgets.TextInputState → List Completion) (state : State) (key : Widgets.Key) : State × Action

Equations

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

def TermColor.Repl.updateMultiline (config : MultilineConfig) (complete : Widgets.TextInputState → List Completion) (state : State) (key : Widgets.Key) : State × Action

Equations

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

def TermColor.Repl.updateWithKeymap (config : Widgets.TextInputConfig) (keymap : Keymap EditorAction) (complete : Widgets.TextInputState → List Completion) (state : State) (key : Widgets.Key) : State × Action

Equations

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

def TermColor.Repl.update (config : Widgets.TextInputConfig) (complete : Widgets.TextInputState → List Completion) (state : State) (key : Widgets.Key) : State × Action

Equations

• TermColor.Repl.update config complete state key = TermColor.Repl.updateWithKeymap config TermColor.Repl.defaultEditorKeymap complete state key