4kusto/vie - Change NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC

optimize Unicode display handling, improve cursor/offset consistency, and cache line/index for rendering

Created by 4kusto on February 3, 2026

NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC

Dependencies

In channels

main

Change contents

Replacement in ViE/Unicode.lean at line 5 [3.10731]
B:BD[3.10884] → [3.10884:10924]
```
def wideRanges : List (Nat × Nat) := [
```
[3.10884]
[3.10924]
```
def wideRangesBmp : Array (Nat × Nat) := #[
```

Replacement in ViE/Unicode.lean at line 18 [3.10731]

B:BD[3.11466] → [3.11466:11514]

  (0xFFE0, 0xFFE6), -- Fullwidth currency/signs

[3.11466]

[3.11514]

  (0xFFE0, 0xFFE6)  -- Fullwidth currency/signs
]
def wideRangesSupplemental : Array (Nat × Nat) := #[

Replacement in ViE/Unicode.lean at line 28 [3.10731]

B:BD[3.11757] → [3.11757:11819]

  wideRanges.any fun (start, stop) => c >= start && c <= stop

[3.11757]

[3.11819]

  if c < 0x1100 then
    false
  else
  let ranges := if c <= 0xFFFF then wideRangesBmp else wideRangesSupplemental
  let rec loop (lo hi : Nat) : Bool :=
    if h : lo < hi then
      let mid := (lo + hi) / 2
      let (start, stop) := ranges[mid]!
      if c < start then
        loop lo mid
      else if c > stop then
        loop (mid + 1) hi
      else
        true
    else
      false
    termination_by hi - lo
  loop 0 ranges.size

Insertion in ViE/Unicode.lean at line 113 [3.10731]

[3.14078]


/-- Convert a display column to a character index (0-based).
    If the column is in the middle of a wide character, it snaps to that character's index. -/
def displayColToCharIndex (s : String) (col : Nat) : Nat :=
  let rec loop (cs : List Char) (idx width : Nat) : Nat :=
    match cs with
    | [] => idx
    | c :: rest =>
      let w := charWidth c
      if width + w > col then
        idx
      else
        loop rest (idx + 1) (width + w)
  loop s.toList 0 0
/-- Display width of the first `idx` characters in a string. -/
def displayWidthAtCharIndex (s : String) (idx : Nat) : Nat :=
  let rec loop (cs : List Char) (i acc : Nat) : Nat :=
    match cs with
    | [] => acc
    | c :: rest =>
      if i >= idx then
        acc
      else
        loop rest (i + 1) (acc + charWidth c)
  loop s.toList 0 0
/-- Convert a display column to a UTF-8 byte offset within a string. -/
def displayColToByteOffset (s : String) (col : Nat) : Nat :=
  let rec loop (cs : List Char) (byteAcc widthAcc : Nat) : Nat :=
    match cs with
    | [] => byteAcc
    | c :: rest =>
      let w := charWidth c
      let b := c.toString.toUTF8.size
      if widthAcc + w > col then
        byteAcc
      else
        loop rest (byteAcc + b) (widthAcc + w)
  loop s.toList 0 0
/-- Build an index mapping display columns to UTF-8 byte offsets at character boundaries.
    The result includes the starting boundary (0,0) and the final boundary (totalWidth,totalBytes). -/
def buildDisplayByteIndex (s : String) : Array (Nat × Nat) :=
  let rec loop (cs : List Char) (disp bytes : Nat) (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=
    match cs with
    | [] => acc
    | c :: rest =>
      let w := charWidth c
      let b := c.toString.toUTF8.size
      let disp' := disp + w
      let bytes' := bytes + b
      loop rest disp' bytes' (acc.push (disp', bytes'))
  loop s.toList 0 0 #[(0, 0)]
/-- Convert a display column to a UTF-8 byte offset using a precomputed index. -/
def displayColToByteOffsetFromIndex (idx : Array (Nat × Nat)) (col : Nat) : Nat :=
  if idx.isEmpty then
    0
  else
    let rec loop (lo hi : Nat) (best : Nat) : Nat :=
      if h : lo < hi then
        let mid := (lo + hi) / 2
        let (disp, bytes) := idx[mid]!
        if col < disp then
          loop lo mid best
        else
          loop (mid + 1) hi bytes
      else
        best
      termination_by hi - lo
    loop 0 idx.size 0
/-- Compute the next display column (advancing by one character). -/
def nextDisplayCol (s : String) (col : Nat) : Nat :=
  let idx := displayColToCharIndex s col
  let startWidth := displayWidthAtCharIndex s idx
  if col < startWidth then
    startWidth
  else
    let chars := s.toList
    if idx < chars.length then
      let w := charWidth (chars[idx]!)
      startWidth + w
    else
      col
/-- Compute the previous display column (moving back by one character). -/
def prevDisplayCol (s : String) (col : Nat) : Nat :=
  if col == 0 then
    0
  else
    let idx := displayColToCharIndex s col
    let startWidth := displayWidthAtCharIndex s idx
    if col > startWidth then
      startWidth
    else if idx == 0 then
      0
    else
      displayWidthAtCharIndex s (idx - 1)
/-- Drop `width` display columns from the start of a substring. -/
def dropByDisplayWidth (s : Substring.Raw) (width : Nat) : Substring.Raw :=
  let rec loop (i : String.Pos.Raw) (acc : Nat) : Substring.Raw :=
    if h : i.byteIdx < s.bsize then
      let c := s.get i
      let w := charWidth c
      if acc + w > width then
        s.extract i ⟨s.bsize⟩
      else
        let i' := s.next i
        have := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)
        loop i' (acc + w)
    else
      s.extract i ⟨s.bsize⟩
    termination_by s.bsize - i.1
  loop 0 0

Insertion in ViE/Unicode.lean at line 232 [3.10731]

[3.14079]

/-- Take characters from substring until visual width limit is reached. -/
def takeByDisplayWidth (s : Substring.Raw) (width : Nat) : String :=
  let rec loop (i : String.Pos.Raw) (currW : Nat) (acc : String) : String :=
    if h : i.byteIdx < s.bsize then
      let c := s.get i
      let w := charWidth c
      if currW + w <= width then
        let i' := s.next i
        have := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)
        loop i' (currW + w) (acc ++ getDisplayString c)
      else
        acc
    else
      acc
    termination_by s.bsize - i.1
  loop 0 0 ""

Replacement in ViE/UI.lean at line 15 [3.14129]

B:BD[3.14527] → [3.14527:14915]

partial def takeVisual (s : Substring.Raw) (width : Nat) : String :=
  let rec loop (sub : Substring.Raw) (currW : Nat) (acc : String) : String :=
    if sub.isEmpty then acc
    else
      let c := sub.front
      let w := Unicode.charWidth c
      if currW + w <= width then
        loop (sub.drop 1) (currW + w) (acc ++ Unicode.getDisplayString c)
      else
        acc
  loop s 0 ""

[3.14527]

[3.14915]

def takeVisual (s : Substring.Raw) (width : Nat) : String :=
  Unicode.takeByDisplayWidth s width

Insertion in ViE/UI.lean at line 55 [3.14129]

[4.640]

           let cachedRaw := buf.cache.findRaw lineIdx
           let cachedIdx := buf.cache.findIndex lineIdx

Replacement in ViE/UI.lean at line 65 [3.14129]

B:BD[2.498] → [2.498:575]

                   let sub := lineStr.toRawSubstring.drop view.scrollCol.val

[2.498]

[2.575]

                   let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val

Replacement in ViE/UI.lean at line 67 [3.14129]

B:BD[2.634] → [2.634:755]

                   let updatedBuf := { buf with cache := buf.cache.update lineIdx dl view.scrollCol.val availableWidth }

[2.634]

[2.755]

                   let cache := match cachedRaw, cachedIdx with
                     | some raw, some idx =>
                       if raw == lineStr then
                         buf.cache
                       else
                         (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                     | _, _ =>
                       (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                   let cache := (cache.update lineIdx dl view.scrollCol.val availableWidth).updateRaw lineIdx lineStr
                   let updatedBuf := { buf with cache := cache }

Replacement in ViE/UI.lean at line 83 [3.14129]

B:BD[4.991] → [4.991:1066]

                 let sub := lineStr.toRawSubstring.drop view.scrollCol.val

[4.838]

[4.1066]

                 let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val

Insertion in ViE/UI.lean at line 85 [3.14129]

[4.1123]

                 let cache := match cachedRaw, cachedIdx with
                   | some raw, some idx =>
                     if raw == lineStr then
                       buf.cache
                     else
                       (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                   | _, _ =>
                     (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))

Replacement in ViE/UI.lean at line 94 [3.14129]

B:BD[4.1169] → [2.1025:1144]

                 let updatedBuf := { buf with cache := buf.cache.update lineIdx dl view.scrollCol.val availableWidth }

[4.1169]

[4.1254]

                 let cache := (cache.update lineIdx dl view.scrollCol.val availableWidth).updateRaw lineIdx lineStr
                 let updatedBuf := { buf with cache := cache }

Replacement in ViE/UI.lean at line 113 [3.14129]
B:BD[4.2015] → [4.2015:2045]
```
             let mut idx := 0
```
[4.2015]
[4.2045]
```
             let mut dispIdx := 0
```

Replacement in ViE/UI.lean at line 115 [3.14129]

B:BD[4.2077] → [4.2077:2204]

                let colVal := view.scrollCol.val + idx
                let isSelected := st.isInSelection lineIdx ⟨colVal⟩

[4.2077]

[3.16481]

                let w := Unicode.charWidth ch
                let colVal := view.scrollCol.val + dispIdx
                let isSelected :=
                  st.isInSelection lineIdx ⟨colVal⟩ ||
                  (w > 1 && st.isInSelection lineIdx ⟨colVal + 1⟩)

Replacement in ViE/UI.lean at line 129 [3.14129]
∅:D[5.692] → [4.2551:2582]
B:BD[4.2551] → [4.2551:2582]
```
                idx := idx + 1
```
[5.692]
[3.17857]
```
                dispIdx := dispIdx + w
```

Replacement in ViE/UI.lean at line 200 [3.14129]

B:BD[3.20406] → [4.3832:3882]

         let buf := getBuffer state view.bufferId

[3.20406]

[3.20450]

--         let buf := getBuffer state view.bufferId

Replacement in ViE/UI.lean at line 206 [3.14129]

B:BD[3.20692] → [4.3883:4026]

∅:D[4.4026] → [3.20782:20988]

B:BD[3.20782] → [3.20782:20988]

             let rIdx : Row := ⟨view.scrollRow.val + visualRow⟩
             if let some currentLineStr := getLineFromBuffer buf rIdx then
               let preCursor := (currentLineStr.toRawSubstring.drop view.scrollCol.val).take (view.cursor.col.val - view.scrollCol.val)
               let visualCol := ViE.Unicode.substringWidth preCursor

[3.20692]

[3.20988]

--             let rIdx : Row := ⟨view.scrollRow.val + visualRow⟩
             if view.cursor.col.val < view.scrollCol.val then
               none
             else
               let visualCol := view.cursor.col.val - view.scrollCol.val

Deletion in ViE/UI.lean at line 214 [3.14129]
B:BD[3.21130] → [3.21130:21153]
```
             else none
```

Insertion in ViE/Types.lean at line 146 [3.22248]

[2.1285]

[4.6229]

  /-- Raw line string cache (no display transform). -/
  rawLineMap : Lean.RBMap Row String compare
  /-- Display-column to byte-offset index cache for a line. -/
  lineIndexMap : Lean.RBMap Row (Array (Nat × Nat)) compare

Insertion in ViE/Types.lean at line 156 [3.22248]

[4.6404]

[2.1361]

  def findRaw (c : RenderCache) (r : Row) : Option String :=
    c.rawLineMap.find? r
  def findIndex (c : RenderCache) (r : Row) : Option (Array (Nat × Nat)) :=
    c.lineIndexMap.find? r

Replacement in ViE/Types.lean at line 163 [3.22248]

B:BD[2.1473] → [2.1473:1542]

    { lineMap := c.lineMap.insert r (s, scrollCol, availableWidth) }

[2.1473]

[4.6723]

    { c with lineMap := c.lineMap.insert r (s, scrollCol, availableWidth) }
  def updateRaw (c : RenderCache) (r : Row) (s : String) : RenderCache :=
    { c with rawLineMap := c.rawLineMap.insert r s }
  def updateIndex (c : RenderCache) (r : Row) (idx : Array (Nat × Nat)) : RenderCache :=
    { c with lineIndexMap := c.lineIndexMap.insert r idx }

Replacement in ViE/Types.lean at line 192 [3.22248]

B:BD[3.26770] → [5.2122:2165]

  cache := { lineMap := Lean.RBMap.empty }

[3.26770]

  cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }

Replacement in ViE/Types.lean at line 200 [3.22248]

B:BD[4.6847] → [5.2166:2224]

    { buf with cache := { lineMap := Lean.RBMap.empty } }

[4.6847]

[3.26882]

    { buf with cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty } }

Insertion in ViE/State/Visual.lean at line 6 [3.32932]
[3.33050]
[3.33050]
```
import ViE.Unicode
```

Replacement in ViE/State/Visual.lean at line 61 [3.32932]

B:BD[4.7886] → [4.7886:7988]

        let sub := line.toRawSubstring.drop minCol |>.take (maxCol - minCol + 1)
        sub.toString

[4.7886]

[4.7988]

        let sub := ViE.Unicode.dropByDisplayWidth line.toRawSubstring minCol
        ViE.Unicode.takeByDisplayWidth sub (maxCol - minCol + 1)

Replacement in ViE/State/Visual.lean at line 66 [3.32932]

B:BD[3.35465] → [4.8025:8224]

      let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0
      let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.length

[3.35465]

[5.2225]

      let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val |>.getD 0
      let lineStr := ViE.getLineFromBuffer buffer p2.row |>.getD ""
      let endCol := if p2.col.val < ViE.Unicode.stringWidth lineStr then
        ViE.Unicode.nextDisplayCol lineStr p2.col.val
      else
        p2.col.val
      let endOff := ViE.getOffsetFromPointInBuffer buffer p2.row.val endCol |>.getD buffer.table.tree.length

Replacement in ViE/State/Visual.lean at line 95 [3.32932]

B:BD[4.8866] → [4.8866:9010]

            let start := lineStart + minCol
            let len := min (maxCol - minCol + 1) (if lineLen > minCol then lineLen - minCol else 0)

[4.8866]

[4.9010]

            let start := ViE.getOffsetFromPointInBuffer buffer r minCol |>.getD (lineStart + lineLen)
            let endCol := maxCol + 1
            let endOff := ViE.getOffsetFromPointInBuffer buffer r endCol |>.getD (lineStart + lineLen)
            let len := if endOff > start then endOff - start else 0

Replacement in ViE/State/Visual.lean at line 107 [3.32932]

B:BD[4.9313] → [4.9313:9516]

        let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0
        let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.length

[4.9313]

[4.9516]

        let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val |>.getD 0
        let lineStr := ViE.getLineFromBuffer buffer p2.row |>.getD ""
        let endCol := if p2.col.val < ViE.Unicode.stringWidth lineStr then
          ViE.Unicode.nextDisplayCol lineStr p2.col.val
        else
          p2.col.val
        let endOff := ViE.getOffsetFromPointInBuffer buffer p2.row.val endCol |>.getD buffer.table.tree.length

Insertion in ViE/State/Movement.lean at line 5 [3.38305]
[3.38397]
[3.38397]
```
import ViE.Unicode
```

Insertion in ViE/State/Movement.lean at line 20 [3.38305]

[3.38893]


def lineString (buffer : FileBuffer) (row : Row) : String :=
  ViE.getLineFromBuffer buffer row |>.getD ""
def lineDisplayWidth (buffer : FileBuffer) (row : Row) : Nat :=
  ViE.getLineLengthFromBuffer buffer row |>.getD 0
def charAtDisplayCol (lineStr : String) (col : Col) : Char :=
  let idx := ViE.Unicode.displayColToCharIndex lineStr col.val
  List.getD lineStr.toList idx ' '
def nextCol (buffer : FileBuffer) (row : Row) (col : Col) : Col :=
  let lineStr := lineString buffer row
  ⟨ViE.Unicode.nextDisplayCol lineStr col.val⟩

Insertion in ViE/State/Movement.lean at line 35 [3.38305]

[3.38894]

def prevCol (buffer : FileBuffer) (row : Row) (col : Col) : Col :=
  let lineStr := lineString buffer row
  ⟨ViE.Unicode.prevDisplayCol lineStr col.val⟩

Replacement in ViE/State/Movement.lean at line 42 [3.38305]

B:BD[3.39098] → [4.9663:9728]

     s.setCursor { cursor with col := ⟨cursor.col.val - 1⟩ }

[3.39098]

[3.39164]

     let newCol := prevCol s.getActiveBuffer cursor.row cursor.col
     s.setCursor { cursor with col := newCol }

Replacement in ViE/State/Movement.lean at line 50 [3.38305]

B:BD[3.39308] → [4.9729:9800]

  let limit := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0

[3.39308]

[3.39379]

  let limit := lineDisplayWidth buffer cursor.row
  let newCol := nextCol buffer cursor.row cursor.col

Replacement in ViE/State/Movement.lean at line 53 [3.38305]

B:BD[3.39380] → [3.39380:39413]

B:BD[3.39413] → [4.9801:9866]

  if cursor.col.val < limit then
     s.setCursor { cursor with col := ⟨cursor.col.val + 1⟩ }

[3.39380]

[3.39479]

  if cursor.col.val < limit && newCol.val != cursor.col.val then
     s.setCursor { cursor with col := newCol }

Replacement in ViE/State/Movement.lean at line 62 [3.38305]

B:BD[4.9916] → [4.9916:9998]

    let lineLen := ViE.getLineLengthFromBuffer s.getActiveBuffer newRow |>.getD 0

[4.9916]

[4.9998]

    let lineLen := lineDisplayWidth s.getActiveBuffer newRow

Replacement in ViE/State/Movement.lean at line 72 [3.38305]

B:BD[4.10135] → [4.10135:10206]

    let lineLen := ViE.getLineLengthFromBuffer buffer newRow |>.getD 0

[4.10135]

[4.10206]

    let lineLen := lineDisplayWidth buffer newRow

Replacement in ViE/State/Movement.lean at line 100 [3.38305]

B:BD[3.41031] → [4.10294:10374]

  let len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0

[3.41031]

[4.10374]

  let len := lineDisplayWidth s.getActiveBuffer cursor.row

Replacement in ViE/State/Movement.lean at line 110 [3.38305]

B:BD[4.10621] → [4.10621:10690]

  let lineLen := ViE.getLineLengthFromBuffer buffer newRow |>.getD 0

[4.10621]

[3.41587]

  let lineLen := lineDisplayWidth buffer newRow

Replacement in ViE/State/Movement.lean at line 123 [3.38305]

B:BD[3.42008] → [4.10816:10896]

  let len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0

[3.42008]

[4.10896]

  let len := lineDisplayWidth s.getActiveBuffer cursor.row

Replacement in ViE/State/Movement.lean at line 128 [3.38305]

B:BD[4.10972] → [4.10972:11052]

  let len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0

[4.10972]

[4.11052]

  let len := lineDisplayWidth s.getActiveBuffer cursor.row

Replacement in ViE/State/Movement.lean at line 149 [3.38305]

B:BD[4.11586] → [4.11586:11654]

    let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0

[4.11586]

[4.11654]

    let lineLen := lineDisplayWidth buffer row

Replacement in ViE/State/Movement.lean at line 156 [3.38305]

B:BD[4.11884] → [4.11884:11961]

         let nextLen := ViE.getLineLengthFromBuffer buffer nextRow |>.getD 0

[4.11884]

[4.11961]

         let nextLen := lineDisplayWidth buffer nextRow

Replacement in ViE/State/Movement.lean at line 164 [3.38305]

B:BD[4.12158] → [4.12158:12275]

      let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
      let c := List.getD lineStr.toList col.val ' '

[4.12158]

[4.12275]

      let lineStr := lineString buffer row
      let c := charAtDisplayCol lineStr col

Replacement in ViE/State/Movement.lean at line 170 [3.38305]

B:BD[4.12388] → [4.12388:12440]

           findNextForward buffer row col.succ true

[4.12388]

[4.12440]

           findNextForward buffer row (nextCol buffer row col) true

Replacement in ViE/State/Movement.lean at line 172 [3.38305]

B:BD[4.12453] → [4.12453:12512]

           findNextWordEndForward buffer row col.succ isKw

[4.12453]

[4.12512]

           findNextWordEndForward buffer row (nextCol buffer row col) isKw

Replacement in ViE/State/Movement.lean at line 175 [3.38305]

B:BD[4.12548] → [4.12548:12604]

            findNextForward buffer row col.succ started

[4.12548]

[4.12604]

            findNextForward buffer row (nextCol buffer row col) started

Replacement in ViE/State/Movement.lean at line 182 [3.38305]

B:BD[4.12786] → [4.12786:12857]

       let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0

[4.12786]

[4.12857]

       let lineLen := lineDisplayWidth buffer row

Replacement in ViE/State/Movement.lean at line 189 [3.38305]

B:BD[4.13052] → [4.13052:13177]

          let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
          let c := List.getD lineStr.toList col.val ' '

[4.13052]

[4.13177]

          let lineStr := lineString buffer row
          let c := charAtDisplayCol lineStr col

Replacement in ViE/State/Movement.lean at line 194 [3.38305]

B:BD[4.13277] → [4.13277:13331]

             findNextForward buffer row col.succ true

[4.13277]

[4.13331]

             findNextForward buffer row (nextCol buffer row col) true

Replacement in ViE/State/Movement.lean at line 198 [3.38305]

B:BD[4.13407] → [4.13407:13469]

             findNextWordEndForward buffer row col.succ wasTv

[4.13407]

[4.13469]

             findNextWordEndForward buffer row (nextCol buffer row col) wasTv

Replacement in ViE/State/Movement.lean at line 205 [3.38305]

B:BD[3.42226] → [4.13622:13699]

  let currLineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0

[3.42226]

[4.13699]

  let currLineLen := lineDisplayWidth buffer cursor.row

Replacement in ViE/State/Movement.lean at line 212 [3.38305]

B:BD[4.13967] → [4.13967:14052]

                   let lineStr := ViE.getLineFromBuffer buffer cursor.row |>.getD ""

[4.13967]

[4.14052]

                   let lineStr := lineString buffer cursor.row

Replacement in ViE/State/Movement.lean at line 214 [3.38305]

B:BD[4.14108] → [4.14108:14184]

                      let ch := List.getD lineStr.toList cursor.col.val ' '

[4.14108]

[4.14184]

                      let ch := charAtDisplayCol lineStr cursor.col

Replacement in ViE/State/Movement.lean at line 218 [3.38305]

B:BD[4.14322] → [4.14322:14402]

                         findNextForward buffer cursor.row cursor.col.succ true

[4.14322]

[4.14402]

                         findNextForward buffer cursor.row (nextCol buffer cursor.row cursor.col) true

Replacement in ViE/State/Movement.lean at line 220 [3.38305]

B:BD[4.14429] → [4.14429:14516]

                         findNextWordEndForward buffer cursor.row cursor.col.succ isKw

[4.14429]

[4.14516]

                         findNextWordEndForward buffer cursor.row (nextCol buffer cursor.row cursor.col) isKw

Replacement in ViE/State/Movement.lean at line 227 [3.38305]

B:BD[4.14775] → [4.14775:14844]

  let finalLineLen := ViE.getLineLengthFromBuffer buffer r |>.getD 0

[4.14775]

[4.14844]

  let finalLineLen := lineDisplayWidth buffer r

Replacement in ViE/State/Movement.lean at line 237 [3.38305]

B:BD[4.15161] → [4.15161:15374]

    partial def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
        let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
        let c := List.getD lineStr.toList col.val ' '

[4.15161]

[4.15374]

  partial def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
        let lineStr := lineString buffer row
        let c := charAtDisplayCol lineStr col

Replacement in ViE/State/Movement.lean at line 244 [3.38305]

B:BD[4.15512] → [4.15512:15597]

                 let prevLen := ViE.getLineLengthFromBuffer buffer prevRow |>.getD 0

[4.15512]

[4.15597]

                 let prevLen := lineDisplayWidth buffer prevRow

Replacement in ViE/State/Movement.lean at line 248 [3.38305]

B:BD[4.15741] → [4.15741:15789]

              findPrevStart buffer row col.pred

[4.15741]

[4.15789]

              findPrevStart buffer row (prevCol buffer row col)

Replacement in ViE/State/Movement.lean at line 255 [3.38305]

B:BD[4.16004] → [4.16004:16125]

        let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
        let c := List.getD lineStr.toList col.val ' '

[4.16004]

[4.16125]

        let lineStr := lineString buffer row
        let c := charAtDisplayCol lineStr col

Replacement in ViE/State/Movement.lean at line 259 [3.38305]
B:BD[4.16206] → [4.16206:16233]
```
           (row, col.succ)
```
[4.16206]
[4.16233]
```
           (row, nextCol buffer row col)
```

Replacement in ViE/State/Movement.lean at line 262 [3.38305]

B:BD[4.16287] → [4.16287:16350]

           else consumeWordBackward buffer row col.pred wantKw

[4.16287]

[4.16350]

           else consumeWordBackward buffer row (prevCol buffer row col) wantKw

Replacement in ViE/State/Movement.lean at line 272 [3.38305]

B:BD[3.42392] → [4.16593:16670]

      let lineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0

[3.42392]

[4.16670]

      let lineLen := lineDisplayWidth buffer cursor.row

Replacement in ViE/State/Movement.lean at line 278 [3.38305]

B:BD[4.16902] → [4.16902:16985]

               let prevLen := ViE.getLineLengthFromBuffer buffer prevRow |>.getD 0

[4.16902]

[4.16985]

               let prevLen := lineDisplayWidth buffer prevRow

Replacement in ViE/State/Movement.lean at line 285 [3.38305]

B:BD[4.17174] → [4.17174:17232]

            findPrevStart buffer cursor.row startCol.pred

[4.17174]

[4.17232]

            findPrevStart buffer cursor.row (prevCol buffer cursor.row startCol)

Replacement in ViE/State/Movement.lean at line 290 [3.38305]

B:BD[4.17282] → [4.17282:17440]

    partial def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
    let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0

[4.17282]

[4.17440]

  partial def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=
    let lineLen := lineDisplayWidth buffer row

Replacement in ViE/State/Movement.lean at line 298 [3.38305]

B:BD[4.17608] → [4.17608:17727]

       let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
       let c := List.getD lineStr.toList col.val ' '

[4.17608]

[4.17727]

       let lineStr := lineString buffer row
       let c := charAtDisplayCol lineStr col

Replacement in ViE/State/Movement.lean at line 301 [3.38305]

B:BD[4.17757] → [4.17757:17799]

          findNextEnd buffer row col.succ

[4.17757]

[4.17799]

          findNextEnd buffer row (nextCol buffer row col)

Replacement in ViE/State/Movement.lean at line 307 [3.38305]

B:BD[4.18005] → [4.18005:18116]

        let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0
        if col.val + 1 >= lineLen then

[4.18005]

[4.18116]

        let lineLen := lineDisplayWidth buffer row
        let nextColVal := (nextCol buffer row col).val
        if nextColVal >= lineLen then

Replacement in ViE/State/Movement.lean at line 312 [3.38305]

B:BD[4.18151] → [4.18151:18288]

           let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""
           let nextC := List.getD lineStr.toList (col.val + 1) ' '

[4.18151]

[4.18288]

           let lineStr := lineString buffer row
           let nextC := charAtDisplayCol lineStr (nextCol buffer row col)

Replacement in ViE/State/Movement.lean at line 318 [3.38305]

B:BD[4.18428] → [4.18428:18486]

              consumeWordToEnd buffer row col.succ wantKw

[4.18428]

[4.18486]

              consumeWordToEnd buffer row (nextCol buffer row col) wantKw

Replacement in ViE/State/Movement.lean at line 325 [3.38305]

B:BD[4.18647] → [4.18647:18724]

  let currLineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0

[4.18647]

[4.18724]

  let currLineLen := lineDisplayWidth buffer cursor.row

Replacement in ViE/State/Movement.lean at line 327 [3.38305]
B:BD[4.18725] → [4.18725:18765]
```
  let startCol : Col := cursor.col.succ
```
[4.18725]
[4.18765]
```
  let startCol : Col := nextCol buffer cursor.row cursor.col
```
Insertion in ViE/State/Edit.lean at line 7 [3.48173]
[4.19234]
[3.48291]
```
import ViE.Unicode
```

Replacement in ViE/State/Edit.lean at line 18 [3.48173]

B:BD[3.48605] → [4.19235:19312]

    match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with

[3.48605]

[6.208]

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with

Replacement in ViE/State/Edit.lean at line 29 [3.48173]

B:BD[6.469] → [4.19377:19454]

    match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with

[6.469]

[6.524]

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with

Insertion in ViE/State/Edit.lean at line 40 [3.48173]

[3.49664]

[6.682]

    let buffer := s.getActiveBuffer
    let prevC := prevCol buffer cursor.row cursor.col

Replacement in ViE/State/Edit.lean at line 43 [3.48173]

B:BD[6.731] → [4.19547:19633]

∅:D[4.19633] → [6.795:962]

B:BD[6.795] → [6.795:962]

       match buffer.table.getOffsetFromPoint cursor.row.val (cursor.col.val - 1) with
       | some offset =>
            { buffer with table := buffer.table.delete offset 1 (offset + 1)
                          dirty := true }
       | none => buffer

[6.731]

[6.962]

       match ViE.getOffsetFromPointInBuffer buffer cursor.row.val prevC.val,
             ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with
       | some startOff, some endOff =>
            let len := endOff - startOff
            if len > 0 then
              { buffer with table := buffer.table.delete startOff len endOff
                            dirty := true }
            else buffer
       | _, _ => buffer

Replacement in ViE/State/Edit.lean at line 53 [3.48173]

B:BD[6.963] → [4.19634:19699]

    s'.setCursor { cursor with col := ⟨cursor.col.val - 1⟩ }

[6.963]

[4.19699]

    s'.setCursor { cursor with col := prevC }

Insertion in ViE/State/Edit.lean at line 76 [3.48173]

[4.20119]

  let buffer := s.getActiveBuffer
  let lineLen := lineDisplayWidth buffer cursor.row
  let nextC := nextCol buffer cursor.row cursor.col

Replacement in ViE/State/Edit.lean at line 80 [3.48173]

B:BD[4.20166] → [4.20166:20264]

    match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with
    | some offset =>

[4.20166]

[4.20264]

    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,
          ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with
    | some startOff, some endOff =>

Replacement in ViE/State/Edit.lean at line 84 [3.48173]

B:BD[4.20378] → [4.20378:20706]

        match buffer.table.getLineRange cursor.row.val with
        | some (_, len) =>
           if cursor.col.val < len then
              { buffer with table := buffer.table.delete offset 1 offset
                            dirty := true }
           else
              buffer
        | none => buffer
     | none => buffer

[4.20378]

[3.50541]

        if cursor.col.val < lineLen && endOff > startOff then
          { buffer with table := buffer.table.delete startOff (endOff - startOff) startOff
                        dirty := true }
        else
          buffer
    | _, _ => buffer

Replacement in ViE/State/Edit.lean at line 93 [3.48173]

B:BD[4.20804] → [4.20804:20879]

  let newLen := ViE.getLineLengthFromBuffer newBuffer cursor.row |>.getD 0

[4.20804]

[4.20879]

  let newLen := lineDisplayWidth newBuffer cursor.row

Replacement in ViE/State/Edit.lean at line 95 [3.48173]

B:BD[4.20928] → [4.20928:20986]

     s'.setCursor { cursor with col := ⟨newLen - 1⟩ }

[4.20928]

[3.50774]

     let lineStr := lineString newBuffer cursor.row
     let newCol := ViE.Unicode.prevDisplayCol lineStr newLen
     s'.setCursor { cursor with col := ⟨newCol⟩ }

Replacement in ViE/State/Edit.lean at line 131 [3.48173]

B:BD[4.21572] → [4.21572:21708]

     match buffer.table.getOffsetFromPoint p1.row.val p1.col.val,
           buffer.table.getOffsetFromPoint p2.row.val p2.col.val with

[4.21572]

[4.21708]

     match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,
           ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with

Replacement in ViE/State/Edit.lean at line 164 [3.48173]

B:BD[4.22796] → [4.22796:22952]

  let lineLen := ViE.getLineLengthFromBuffer buffer endP.row |>.getD 0
  let targetCol := if endP.col.val + 1 <= lineLen then endP.col.val + 1 else lineLen

[4.22796]

[4.22952]

  let lineLen := lineDisplayWidth buffer endP.row
  let lineStr := lineString buffer endP.row
  let targetCol := if endP.col.val < lineLen then ViE.Unicode.nextDisplayCol lineStr endP.col.val else lineLen

Replacement in ViE/State/Edit.lean at line 205 [3.48173]

B:BD[6.2475] → [4.23934:24036]

      let (offset, textToInsert) := match buffer.table.getOffsetFromPoint (cursor.row.val + 1) 0 with

[6.2475]

[4.24036]

      let (offset, textToInsert) := match ViE.getOffsetFromPointInBuffer buffer (cursor.row.val + 1) 0 with

Replacement in ViE/State/Edit.lean at line 231 [3.48173]

B:BD[6.3142] → [4.24805:24885]

      let offset := match buffer.table.getOffsetFromPoint cursor.row.val 0 with

[6.3142]

[6.3211]

      let offset := match ViE.getOffsetFromPointInBuffer buffer cursor.row.val 0 with

Replacement in ViE/State/Edit.lean at line 244 [3.48173]

B:BD[4.25056] → [4.25056:25149]

  let currentOffset := match buf.table.getOffsetFromPoint cursor.row.val cursor.col.val with

[4.25056]

[6.3698]

  let currentOffset := match ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val with

Replacement in ViE/State/Edit.lean at line 262 [3.48173]

B:BD[4.25244] → [4.25244:25337]

  let currentOffset := match buf.table.getOffsetFromPoint cursor.row.val cursor.col.val with

[4.25244]

[6.4387]

  let currentOffset := match ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val with

Replacement in ViE/State/Config.lean at line 46 [3.53268]

B:BD[3.54141] → [5.2502:2545]

  cache := { lineMap := Lean.RBMap.empty }

[3.54141]

  cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }

Insertion in ViE/Data/PieceTable.lean at line 3 [3.73967]
[3.74066]
[3.74066]
```
import ViE.Unicode
```

Replacement in ViE/Data/PieceTable.lean at line 160 [3.73967]

B:BD[6.7985] → [7.4449:4490]

∅:D[7.4490] → [6.8055:8102]

B:BD[6.8055] → [6.8055:8102]

B:BD[6.8102] → [7.4491:4524]

      -- Allow col up to len (inclusive)
      if col <= len then some (startOff + col)
      else some (startOff + len)

[6.7985]

[6.8296]

      -- Col is a display column; convert to byte offset within the line.
      let lineStr := PieceTree.getSubstring pt.tree startOff len pt
      let byteOff := ViE.Unicode.displayColToByteOffset lineStr col
      let clamped := if byteOff <= len then byteOff else len
      some (startOff + clamped)

Replacement in ViE/Data/PieceTable.lean at line 204 [3.73967]

B:BD[6.9204] → [6.9204:9230]

  | some (r, c) => (r, c)

[6.9204]

[6.9230]

  | some (r, c) =>
    match PieceTable.getLineRange pt r with
    | some (startOff, len) =>
      let rel := if c <= len then c else len
      let sub := PieceTree.getSubstring pt.tree startOff rel pt
      let displayCol := ViE.Unicode.stringWidth sub
      (r, displayCol)
    | none => (r, c)

Replacement in ViE/Buffer/LowIO.lean at line 21 [3.119821]

B:BD[3.120337] → [5.3676:3727]

          cache := { lineMap := Lean.RBMap.empty }

[3.120337]

          cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }

Replacement in ViE/Buffer/LowIO.lean at line 38 [3.119821]

B:BD[3.120782] → [5.3728:3779]

          cache := { lineMap := Lean.RBMap.empty }

[3.120782]

          cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }

Replacement in ViE/Buffer/LowIO.lean at line 48 [3.119821]

B:BD[3.121008] → [5.3780:3829]

        cache := { lineMap := Lean.RBMap.empty }

[3.121008]

        cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }

Replacement in ViE/Buffer/LowIO.lean at line 58 [3.119821]

B:BD[3.121212] → [5.3830:3877]

      cache := { lineMap := Lean.RBMap.empty }

[3.121212]

      cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }

Insertion in ViE/Buffer/Content.lean at line 5 [3.121265]
[3.121327]
[3.121327]
```
import ViE.Unicode
```

Replacement in ViE/Buffer/Content.lean at line 13 [3.121265]

B:BD[4.28792] → [4.28792:28821]

  buffer.table.getLine n.val

[4.28792]

[3.121522]

  match buffer.cache.findRaw n with
  | some s => some s
  | none => buffer.table.getLine n.val
/-- Get byte offset from Row/Col (display column) using per-line index cache if available. -/
def getOffsetFromPointInBuffer (buffer : FileBuffer) (row col : Nat) : Option Nat :=
  match buffer.table.getLineRange row with
  | some (startOff, len) =>
      let line := getLineFromBuffer buffer ⟨row⟩ |>.getD ""
      let byteOff := match buffer.cache.findIndex ⟨row⟩ with
        | some idx => ViE.Unicode.displayColToByteOffsetFromIndex idx col
        | none => ViE.Unicode.displayColToByteOffset line col
      let clamped := if byteOff <= len then byteOff else len
      some (startOff + clamped)
  | none => none

Replacement in ViE/Buffer/Content.lean at line 31 [3.121265]

B:BD[4.28898] → [4.28898:28933]

  buffer.table.getLineLength n.val

[4.28898]

[3.121695]

  match getLineFromBuffer buffer n with
  | some line => some (ViE.Unicode.stringWidth line)
  | none => none

Replacement in ViE/Buffer/Content.lean at line 60 [3.121265]

B:BD[3.122658] → [5.3893:3938]

    cache := { lineMap := Lean.RBMap.empty }

[3.122658]

    cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }

Replacement in ViE/Buffer/Content.lean at line 74 [3.121265]
B:BD[3.123179] → [4.29159:29204]
```
     match buffer.table.getLine row.val with
```
[3.123179]
[3.123220]
```
     match getLineFromBuffer buffer row with
```

Replacement in ViE/App.lean at line 113 [3.125244]

B:BD[3.128481] → [5.3954:4003]

        cache := { lineMap := Lean.RBMap.empty }

[3.128481]

        cache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }