TermColor.Repl.Keymap

Inspectable, ordered keyboard bindings. Contexts are values rather than callbacks, so a keymap is plain data: an application supplies the active context values for its current model.

structure TermColor.Repl.KeyContext : Type

A validated name for an active keybinding context.

• name : String

def TermColor.Repl.instReprKeyContext.repr : KeyContext → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instReprKeyContext : Repr KeyContext

Equations

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

@[instance_reducible]

instance TermColor.Repl.instBEqKeyContext : BEq KeyContext

Equations

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

def TermColor.Repl.instBEqKeyContext.beq : KeyContext → KeyContext → Bool

Equations

• TermColor.Repl.instBEqKeyContext.beq { name := a } { name := b } = (a == b)
• TermColor.Repl.instBEqKeyContext.beq x✝¹ x✝ = false

def TermColor.Repl.instDecidableEqKeyContext.decEq (x✝ x✝¹ : KeyContext) : Decidable (x✝ = x✝¹)

Equations

• TermColor.Repl.instDecidableEqKeyContext.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.Repl.instDecidableEqKeyContext : DecidableEq KeyContext

Equations

• TermColor.Repl.instDecidableEqKeyContext = TermColor.Repl.instDecidableEqKeyContext.decEq

def TermColor.Repl.KeyContext.ofString (name : String) : KeyContext

Construct an application context from one centralized name.

Equations

• TermColor.Repl.KeyContext.ofString name = { name := name }

def TermColor.Repl.KeyContext.editor : KeyContext

Equations

• TermColor.Repl.KeyContext.editor = TermColor.Repl.KeyContext.ofString "editor"

def TermColor.Repl.KeyContext.completion : KeyContext

Equations

• TermColor.Repl.KeyContext.completion = TermColor.Repl.KeyContext.ofString "completion"

def TermColor.Repl.KeyContext.multiline : KeyContext

Equations

• TermColor.Repl.KeyContext.multiline = TermColor.Repl.KeyContext.ofString "multiline"

structure TermColor.Repl.KeyBinding (Action : Type) : Type

• key : Widgets.Key
• action : Action
• context : Option KeyContext
• label : String
• description : String

@[instance_reducible]

instance TermColor.Repl.instReprKeyBinding {Action✝ : Type} [Repr Action✝] : Repr (KeyBinding Action✝)

Equations

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

def TermColor.Repl.instReprKeyBinding.repr {Action✝ : Type} [Repr Action✝] : KeyBinding Action✝ → Nat → Std.Format

Equations

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

structure TermColor.Repl.Keymap (Action : Type) : Type

• bindings : List (KeyBinding Action)

@[instance_reducible]

instance TermColor.Repl.instReprKeymap {Action✝ : Type} [Repr Action✝] : Repr (Keymap Action✝)

Equations

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

def TermColor.Repl.instReprKeymap.repr {Action✝ : Type} [Repr Action✝] : Keymap Action✝ → Nat → Std.Format

Equations

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

structure TermColor.Repl.BindingSpec (Action : Type) : Type

One declarative action binding. Multiple physical keys may name one action.

• keys : List Widgets.Key
• action : Action
• context : Option KeyContext
• label : String
• description : String

@[instance_reducible]

instance TermColor.Repl.instReprBindingSpec {Action✝ : Type} [Repr Action✝] : Repr (BindingSpec Action✝)

Equations

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

def TermColor.Repl.instReprBindingSpec.repr {Action✝ : Type} [Repr Action✝] : BindingSpec Action✝ → Nat → Std.Format

Equations

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

def TermColor.Repl.BindingSpec.expand {Action : Type} (spec : BindingSpec Action) : List (KeyBinding Action)

Equations

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

def TermColor.Repl.Keymap.fromSpecs {Action : Type} (specs : List (BindingSpec Action)) : Keymap Action

Equations

• TermColor.Repl.Keymap.fromSpecs specs = { bindings := List.flatMap TermColor.Repl.BindingSpec.expand specs }

def TermColor.Repl.Keymap.resolveBinding {Action : Type} (keymap : Keymap Action) (contexts : List KeyContext) (key : Widgets.Key) : Option (KeyBinding Action)

First matching binding wins; list order is the precedence contract.

Equations

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

def TermColor.Repl.Keymap.resolve {Action : Type} (keymap : Keymap Action) (contexts : List KeyContext) (key : Widgets.Key) : Option Action

Resolve the first matching action.

Equations

• keymap.resolve contexts key = Option.map (fun (x : TermColor.Repl.KeyBinding Action) => x.action) (keymap.resolveBinding contexts key)

def TermColor.Repl.Keymap.visible {Action : Type} (keymap : Keymap Action) (contexts : List KeyContext) : List (KeyBinding Action)

Equations

• keymap.visible contexts = List.filter (fun (binding : TermColor.Repl.KeyBinding Action) => TermColor.Repl.Keymap.active✝ contexts binding.context) keymap.bindings

def TermColor.Repl.Keymap.keys {Action : Type} (keymap : Keymap Action) : List Widgets.Key

Equations

• keymap.keys = List.map (fun (x : TermColor.Repl.KeyBinding Action) => x.key) keymap.bindings

def TermColor.Repl.Keymap.conflicts {Action : Type} (keymap : Keymap Action) : List (Widgets.Key × Option KeyContext)

Return duplicate key/context pairs that rely on implicit first-match precedence.

Equations

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

def TermColor.Repl.Keymap.keyLabel : Widgets.Key → String

Equations

• TermColor.Repl.Keymap.keyLabel (TermColor.Widgets.Key.char value) = toString value
• TermColor.Repl.Keymap.keyLabel (TermColor.Widgets.Key.ctrl value) = toString "Ctrl-" ++ toString value
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.left = "←"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.right = "→"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.home = "Home"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.end = "End"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.up = "↑"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.down = "↓"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.pageUp = "PgUp"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.pageDown = "PgDn"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.enter = "Enter"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.backspace = "Backspace"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.delete = "Delete"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.tab = "Tab"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.shiftTab = "Shift-Tab"
• TermColor.Repl.Keymap.keyLabel TermColor.Widgets.Key.escape = "Esc"

Built-in editor bindings

inductive TermColor.Repl.EditorAction : Type

• complete : EditorAction
• completionNext : EditorAction
• completionPrevious : EditorAction
• dismissCompletion : EditorAction
• historyPrevious : EditorAction
• historyNext : EditorAction
• lineBreak : EditorAction
• submit : EditorAction
• quit : EditorAction
• forceQuit : EditorAction

def TermColor.Repl.instReprEditorAction.repr : EditorAction → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instReprEditorAction : Repr EditorAction

Equations

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

def TermColor.Repl.instBEqEditorAction.beq : EditorAction → EditorAction → Bool

Equations

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

@[instance_reducible]

instance TermColor.Repl.instBEqEditorAction : BEq EditorAction

Equations

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

@[instance_reducible]

instance TermColor.Repl.instDecidableEqEditorAction : DecidableEq EditorAction

Equations

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

structure TermColor.Repl.EditorContext : Type

• completionOpen : Bool
• multiline : Bool

def TermColor.Repl.instReprEditorContext.repr : EditorContext → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.Repl.instReprEditorContext : Repr EditorContext

Equations

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

@[instance_reducible]

instance TermColor.Repl.instBEqEditorContext : BEq EditorContext

Equations

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

def TermColor.Repl.instBEqEditorContext.beq : EditorContext → EditorContext → Bool

Equations

• TermColor.Repl.instBEqEditorContext.beq { completionOpen := a, multiline := a_1 } { completionOpen := b, multiline := b_1 } = (a == b && a_1 == b_1)
• TermColor.Repl.instBEqEditorContext.beq x✝¹ x✝ = false

def TermColor.Repl.instDecidableEqEditorContext.decEq (x✝ x✝¹ : EditorContext) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.Repl.instDecidableEqEditorContext : DecidableEq EditorContext

Equations

• TermColor.Repl.instDecidableEqEditorContext = TermColor.Repl.instDecidableEqEditorContext.decEq

def TermColor.Repl.editorContexts (context : EditorContext) : List KeyContext

Equations

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

def TermColor.Repl.defaultEditorKeymap (lineBreak : Widgets.Key := Widgets.Key.ctrl 'n') : Keymap EditorAction

Equations

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