4kusto/vie - Change 4GUZZYJSWKA44VKYZ2U3G7SQ32JHHHPBSYUWWNNWWBOEDUN7RLKAC

Implement linewise visual mode for Vim-compatible V behavior

Created by 4kusto on March 6, 2026

4GUZZYJSWKA44VKYZ2U3G7SQ32JHHHPBSYUWWNNWWBOEDUN7RLKAC

Dependencies

In channels

main

Change contents

Replacement in ViE/UI/Window.lean at line 87 [4.1840]

B:BD[4.5995] → [4.5995:6077]

      let isVisual := state.mode == Mode.visual || state.mode == Mode.visualBlock

[4.5995]

[4.6077]

      let isVisual := state.mode == Mode.visual || state.mode == Mode.visualLine || state.mode == Mode.visualBlock

Replacement in ViE/UI/Window.lean at line 199 [4.1840]

B:BD[4.10713] → [4.10713:10785]

  let isVisual := st.mode == Mode.visual || st.mode == Mode.visualBlock

[4.10713]

[4.10785]

  let isVisual := st.mode == Mode.visual || st.mode == Mode.visualLine || st.mode == Mode.visualBlock

Replacement in ViE/UI/Render.lean at line 178 [4.17442]

B:BD[4.24705] → [4.24705:24789]

  if stateAfterLayout.mode == .visual || stateAfterLayout.mode == .visualBlock then

[4.24705]

[4.24789]

  if stateAfterLayout.mode == .visual || stateAfterLayout.mode == .visualLine || stateAfterLayout.mode == .visualBlock then

Insertion in ViE/Types.lean at line 14 [5.22248]
[5.22379]
[5.22379]
```
  | visualLine
```
Insertion in ViE/Types.lean at line 26 [5.22248]
[5.22576]
[5.22576]
```
    | .visualLine => "VISUAL LINE"
```

Insertion in ViE/State/Visual.lean at line 13 [5.32932]

[5.33253]


def EditorState.startVisualLineMode (s : EditorState) : EditorState :=
  let s' := s.clampCursor
  { s' with mode := .visualLine, selectionStart := some s'.getCursor, message := "-- VISUAL LINE --" }

Insertion in ViE/State/Visual.lean at line 27 [5.32932]

[5.33741]


private def firstNonBlankCol (line : String) (tabStop : Nat) : Nat :=
  let rec loop (cs : List Char) (col : Nat) : Nat :=
    match cs with
    | [] => 0
    | c :: rest =>
      if c == ' ' || c == '\t' then
        loop rest (col + ViE.Unicode.charWidthAt tabStop col c)
      else
        col
  loop line.toList 0

Insertion in ViE/State/Visual.lean at line 50 [5.32932]

[6.7124]

[5.34232]

    else if s.mode == .visualLine then
       let cursor := s.getCursor
       let minRow := min startPt.row cursor.row
       let maxRow := max startPt.row cursor.row
       row >= minRow && row <= maxRow

Insertion in ViE/State/Visual.lean at line 85 [5.32932]

[6.8024]

[5.35399]

    else if s.mode == .visualLine then
      let cursor := s.getCursor
      let minRow := (min startPt.row cursor.row).val
      let maxRow := (max startPt.row cursor.row).val
      let lines := (List.range (maxRow - minRow + 1)).map fun i =>
        ViE.getLineFromBuffer buffer ⟨minRow + i⟩ |>.getD ""
      if lines.isEmpty then "" else String.intercalate "\n" lines ++ "\n"

Insertion in ViE/State/Visual.lean at line 115 [5.32932]

[7.8076]

      }
    else if s.mode == .visualLine then
      {
        kind := .linewise
        text := text
        blockLines := []
        blockWidth := 0

Insertion in ViE/State/Visual.lean at line 167 [5.32932]

[7.8727]

[5.37367]

    else if s.mode == .visualLine then
      let cursor := s.getCursor
      let minRow := (min startPt.row cursor.row).val
      let maxRow := (max startPt.row cursor.row).val
      let text := s.getSelectedText
      let reg : Register := {
        kind := .linewise
        text := text
        blockLines := []
        blockWidth := 0
      }
      let s' := s.updateActiveBuffer fun buffer =>
        match buffer.table.getLineRange minRow with
        | some (startOff, _) =>
            let endOff :=
              match buffer.table.getLineRange (maxRow + 1) with
              | some (nextStart, _) => nextStart
              | none => buffer.table.tree.length
            let len := endOff - startOff
            if len > 0 then
              { buffer with table := buffer.table.delete startOff len startOff, dirty := true }
            else
              buffer
        | none => buffer
      let newBuffer := s'.getActiveBuffer
      let newRowVal := min minRow (newBuffer.lineCount.pred)
      let newRow : Row := ⟨newRowVal⟩
      let lineStr := ViE.getLineFromBuffer newBuffer newRow |>.getD ""
      let newCol := firstNonBlankCol lineStr tabStop
      { s'.exitVisualMode with clipboard := some reg } |>.setCursor { row := newRow, col := ⟨newCol⟩ }

Replacement in ViE/Lsp/Lean.lean at line 891 [8.7243]

B:BD[8.23950] → [8.23950:23992]

    | .normal | .visual | .visualBlock =>

[8.23950]

[8.23992]

    | .normal | .visual | .visualLine | .visualBlock =>

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

B:BD[4.52597] → [2.1801:1860]

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

[4.52597]

[2.1860]

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

Insertion in ViE/Key/Map.lean at line 636 [5.56987]

[5.63351]

    | Key.char 'V' =>
        if s.mode == .visualLine then
          pure $ EditorState.exitVisualMode s
        else
          pure $ EditorState.startVisualLineMode s

Insertion in ViE/Key/Dispatch.lean at line 18 [5.71713]
[5.72134]
[5.72134]
```
  | .visualLine => config.bindings.visual state k
```
Insertion in ViE/Config.lean at line 62 [5.95659]
[5.101779]
[5.101779]
```
  | .visualLine => config.bindings.visual state k
```
Insertion in ViE/BlikuAdapter.lean at line 5 [9.2460]
[9.2538]
[9.2538]
```
import ViE.Unicode
```

Replacement in ViE/BlikuAdapter.lean at line 180 [9.2460]

B:BD[3.7337] → [3.7337:7403]

      if state.mode == .visual || state.mode == .visualBlock then

[3.7337]

[3.7403]

      if state.mode == .visual || state.mode == .visualLine || state.mode == .visualBlock then
        let cursor :=
          if state.mode == .visualLine then
            let activeBuf := state.getActiveBuffer
            let anchorRow := anchor.row.val
            let cursorRow := state.getCursor.row.val
            let endRow := max anchorRow cursorRow
            let endLine := ViE.getLineFromBuffer activeBuf ⟨endRow⟩ |>.getD ""
            let endCol := ViE.Unicode.stringWidthWithTabStop endLine state.config.tabStop
            { row := endRow, col := endCol }
          else
            toBlikuCursor state.getCursor
        let anchor' :=
          if state.mode == .visualLine then
            let anchorRow := anchor.row.val
            let cursorRow := state.getCursor.row.val
            { row := min anchorRow cursorRow, col := 0 }
          else
            toBlikuCursor anchor

Replacement in ViE/BlikuAdapter.lean at line 200 [9.2460]

B:BD[3.7418] → [3.7418:7509]

          anchor := toBlikuCursor anchor
          cursor := toBlikuCursor state.getCursor

[3.7418]

[3.7509]

          anchor := anchor'
          cursor := cursor

Replacement in Test/Keybinds.lean at line 121 [6.32086]

B:BD[2.2463] → [2.2463:2521]

  assertEqual "V enters visual mode" Mode.visual s_V.mode

[2.2463]

[10.37353]

  assertEqual "V enters visual line mode" Mode.visualLine s_V.mode

Insertion in Test/Keybinds.lean at line 236 [6.32086]

[7.65442]

  let s_linewise0 ← runKeys s0 ([Key.char 'i'] ++ keys "aa\nbb\ncc" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g'])
  let s_linewiseD ← runKeys s_linewise0 [Key.char 'V', Key.char 'j', Key.char 'd']
  assertBuffer "visual line d deletes full lines" s_linewiseD "cc"
  match s_linewiseD.clipboard with
  | some reg =>
      assertEqual "visual line d register kind" RegisterKind.linewise reg.kind
      assertEqual "visual line d register text" "aa\nbb\n" reg.text
  | none => assertEqual "visual line d register set" true false
  let s_linewiseY ← runKeys s_linewise0 [Key.char 'V', Key.char 'j', Key.char 'y']
  let s_linewiseP ← runKeys s_linewiseY [Key.char 'G', Key.char 'p']
  assertBuffer "visual line y/p pastes linewise" s_linewiseP "aa\nbb\ncc\naa\nbb\n"

Replacement in Main.lean at line 24 [5.134883]
B:BD[3.13272] → [3.13272:13307]
```
  explorerPreviewSplitRatio := 0.5
```
[3.13272]
[3.13307]
```
  explorerPreviewSplitRatio := 0.3
```