4kusto/vie - Change ZSBXK2GGVYHLXXMAIIEXW45COI3GSP5CLBRUSY5JNRDSHTLGGBVAC

align keybindings closer to Vim: reserve q for macros, map V to visual and Ctrl-v to visual-block, and update keybind/docs/tests

Created by 4kusto on February 25, 2026

ZSBXK2GGVYHLXXMAIIEXW45COI3GSP5CLBRUSY5JNRDSHTLGGBVAC

Dependencies

In channels

main

Change contents

Insertion in ViE/Lsp/Lean.lean at line 111 [3.7243]

[2.1251]

[3.8761]

private def resolvePathForUri (workspaceRoot : Option String) (path : String) : IO String := do
  let candidate : System.FilePath ←
    if path.startsWith "/" then
      pure (System.FilePath.mk path)
    else
      match workspaceRoot with
      | some root =>
          pure <| System.FilePath.mk (root ++ "/" ++ path)
      | none =>
          let cwd ← IO.currentDir
          pure <| System.FilePath.mk (cwd.toString ++ "/" ++ path)
  try
    let rp ← IO.FS.realPath candidate
    pure rp.toString
  catch _ =>
    pure candidate.normalize.toString
def fileUriWithWorkspace (workspaceRoot : Option String) (path : String) : IO String := do
  let absPath ← resolvePathForUri workspaceRoot path
  pure (fileUri absPath)

Replacement in ViE/Lsp/Lean.lean at line 598 [3.7243]
B:BD[3.14373] → [3.14373:14390]
```
  let rootUri :=
```
[3.14373]
[3.14390]
```
  let rootUri ←
```

Replacement in ViE/Lsp/Lean.lean at line 600 [3.7243]

B:BD[3.14422] → [3.14422:14493]

    | some p => Lean.Json.str (fileUri p)
    | none => Lean.Json.null

[3.14422]

[3.14493]

    | some p => do
        let uri ← fileUriWithWorkspace none p
        pure (Lean.Json.str uri)
    | none =>
        pure Lean.Json.null

Replacement in ViE/Lsp/Lean.lean at line 628 [3.7243]

B:BD[3.15155] → [3.15155:15187]

        let uri := fileUri path

[3.15155]

[3.15187]

        let uri ← fileUriWithWorkspace session.rootPath path

Replacement in ViE/Lsp/Lean.lean at line 930 [3.7243]

B:BD[3.25206] → [3.25206:25242]

            let uri := fileUri path

[3.25206]

[3.25242]

            let uri ← fileUriWithWorkspace s.rootPath path

Replacement in ViE/Lsp/Lean.lean at line 1046 [3.7243]

∅:D[4.5415] → [5.9258:9298]

B:BD[5.9258] → [5.9258:9298]

                let uri := fileUri path

[4.5415]

[5.9298]

                let uri ← fileUriWithWorkspace s.rootPath path

Replacement in ViE/Lsp/Lean.lean at line 1066 [3.7243]
B:BD[5.9800] → [5.9800:9827]
```
      let matchesActive :=
```
[5.9800]
[5.9827]
```
      let matchesActive ←
```

Replacement in ViE/Lsp/Lean.lean at line 1068 [3.7243]

B:BD[5.9877] → [5.9877:9944]

        | some path => fileUri path == uri
        | none => false

[5.9877]

[5.9944]

        | some path =>
            let activeUri ← fileUriWithWorkspace state.getCurrentWorkspace.rootPath path
            pure (activeUri == uri)
        | none =>
            pure false

Replacement in ViE/Lsp/Lean.lean at line 1080 [3.7243]

∅:D[5.10270] → [3.26233:26351]

B:BD[3.26233] → [3.26233:26351]

private def formatInfoViewContent (tabStop : Nat) (sourceView : ViewState) (sourceBuf : FileBuffer) : IO String := do

[5.10270]

[3.26351]

private def formatInfoViewContent (workspaceRoot : Option String) (tabStop : Nat) (sourceView : ViewState) (sourceBuf : FileBuffer) : IO String := do

Replacement in ViE/Lsp/Lean.lean at line 1092 [3.7243]

B:BD[3.26705] → [3.26705:26783]

  let uri := match sourceBuf.filename with | some p => fileUri p | none => ""

[3.26705]

[3.26783]

  let uri ←
    match sourceBuf.filename with
    | some p => fileUriWithWorkspace workspaceRoot p
    | none => pure ""

Replacement in ViE/Lsp/Lean.lean at line 1131 [3.7243]

B:BD[3.28091] → [3.28091:28173]

  let content ← formatInfoViewContent state.config.tabStop sourceView sourceBuf

[3.28091]

[3.28173]

  let content ← formatInfoViewContent state.getCurrentWorkspace.rootPath state.config.tabStop sourceView sourceBuf

Replacement in ViE/Key/Map.lean at line 356 [8.56987]

B:BD[6.23846] → [7.52324:52376]

    | Key.char 'q' => pure $ s.setMode Mode.command

[6.23846]

[7.52376]

    | Key.char 'q' => pure { s with message := "macro recording not implemented", dirty := true }

Replacement in ViE/Key/Map.lean at line 360 [8.56987]

B:BD[7.52597] → [7.52597:52661]

    | Key.char 'V' => pure $ EditorState.startVisualBlockMode s

[7.52597]

[7.52661]

    | Key.char 'V' => pure $ EditorState.startVisualMode s
    | Key.ctrl 'v' => pure $ EditorState.startVisualBlockMode s

Insertion in Test/Lsp.lean at line 21 [2.3520]

[2.4274]

  let uriWs ← ViE.Lsp.Lean.fileUriWithWorkspace (some "/tmp/ws") "dir/a b.lean"
  assertEqual "fileUriWithWorkspace resolves relative path from workspace root" "file:///tmp/ws/dir/a%20b.lean" uriWs
  let uriWsAbs ← ViE.Lsp.Lean.fileUriWithWorkspace (some "/tmp/ws") "/tmp/alt/x.lean"
  assertEqual "fileUriWithWorkspace keeps absolute path priority" "file:///tmp/alt/x.lean" uriWsAbs

Insertion in Test/Keybinds.lean at line 116 [11.32086]

[9.12074]

[10.37353]


  let s_q ← runKeys s0 [Key.char 'q']
  assertEqual "q does not enter command mode" Mode.normal s_q.mode
  let s_V ← runKeys s0 [Key.char 'V']
  assertEqual "V enters visual mode" Mode.visual s_V.mode

Insertion in Test/Keybinds.lean at line 123 [11.32086]

[10.37354]

  let s_ctrlV ← runKeys s0 [Key.ctrl 'v']
  assertEqual "Ctrl-v enters visual block mode" Mode.visualBlock s_ctrlV.mode

Replacement in Test/Keybinds.lean at line 248 [11.32086]

B:BD[6.66136] → [6.66136:66239]

  let s_blkY ← runKeys s_blk0 [Key.char 'l', Key.char 'V', Key.char 'l', Key.char 'j', Key.char 'y']

[6.66136]

[6.66239]

  let s_blkY ← runKeys s_blk0 [Key.char 'l', Key.ctrl 'v', Key.char 'l', Key.char 'j', Key.char 'y']

Replacement in Test/Keybinds.lean at line 258 [11.32086]

B:BD[6.66824] → [6.66824:66928]

  let s_blkD ← runKeys s_blkD0 [Key.char 'l', Key.char 'V', Key.char 'l', Key.char 'j', Key.char 'd']

[6.66824]

[6.66928]

  let s_blkD ← runKeys s_blkD0 [Key.char 'l', Key.ctrl 'v', Key.char 'l', Key.char 'j', Key.char 'd']

Replacement in Test/Keybinds.lean at line 742 [11.32086]

B:BD[7.115066] → [7.115066:115163]

  let s30 ← runKeys s29 [Key.char 'l', Key.char 'V', Key.char 'l', Key.char 'j', Key.char 'd']

[7.115066]

[7.115163]

  let s30 ← runKeys s29 [Key.char 'l', Key.ctrl 'v', Key.char 'l', Key.char 'j', Key.char 'd']

Replacement in README.md at line 55 [8.132959]
B:BD[12.835] → [12.835:869]
```
- `q`: Enter Command Mode (alias)
```
[12.835]
[12.869]
```
- `q`: (reserved for macro recording; not implemented)
```
Replacement in README.md at line 60 [8.132959]
B:BD[12.940] → [12.940:970]
```
- `V`: Enter VisualBlock Mode
```
[12.940]
[12.970]
```
- `V`: Enter Visual Mode
- `Ctrl-v`: Enter VisualBlock Mode
```