4kusto/vie - Change MDJSREIO7F3IHOEGBAZBS4VIFPV2ETK6BAEM64AO2P5OBV6XOF2QC

fix Lean completion LSP position to UTF-16 columns, ignore stale completion responses, and clear completion state on mode transitions

Created by 4kusto on February 19, 2026

MDJSREIO7F3IHOEGBAZBS4VIFPV2ETK6BAEM64AO2P5OBV6XOF2QC

Dependencies

In channels

main

Change contents

Insertion in ViE/Lsp/Lean.lean at line 40 [3.7243]
[2.78]
[3.7945]
```
  latestCompletionReqId : Option Nat := none
```
Insertion in ViE/Lsp/Lean.lean at line 58 [3.7243]
[4.3177]
[3.8389]
```
    latestCompletionReqId := none
```
Insertion in ViE/Lsp/Lean.lean at line 193 [3.7243]
[4.3244]
[3.9470]
```
    latestCompletionReqId := none
```
Insertion in ViE/Lsp/Lean.lean at line 475 [3.7243]
[4.4253]
[4.4253]
```
  let isLatest := st.latestCompletionReqId == some reqId
```

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

B:BD[2.4374] → [2.4374:4457]

∅:D[2.4457] → [4.4436:4518]

B:BD[4.4436] → [4.4436:4518]

B:BD[4.4518] → [2.4458:4550]

∅:D[2.4550] → [4.4618:4707]

B:BD[4.4618] → [4.4618:4707]

      let items := rankAndSelectCompletions query (parseCompletionItems result) 40
      let completion :=
        if items.isEmpty then
          none
        else
          some (uri, { items := items, selected := 0, anchorRow := row, anchorCol := col })
      uiStateRef.set { st with pendingCompletion := pending', completion := completion }

[2.4374]

[4.4707]

      if !isLatest then
        uiStateRef.set { st with pendingCompletion := pending' }
      else
        let items := rankAndSelectCompletions query (parseCompletionItems result) 40
        let completion :=
          if items.isEmpty then
            none
          else
            some (uri, { items := items, selected := 0, anchorRow := row, anchorCol := col })
        uiStateRef.set {
          st with
            pendingCompletion := pending'
            latestCompletionReqId := none
            completion := completion
        }

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

[3.13597]

[4.4998]

            let clearCompletion := st.latestCompletionReqId == some reqId

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

[4.5179]

                latestCompletionReqId := if clearCompletion then none else st.latestCompletionReqId
                completion := if clearCompletion then none else st.completion

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

B:BD[4.5728] → [2.4681:4788]

  uiStateRef.set { st with pendingCompletion := st.pendingCompletion.insert reqId (uri, row, col, query) }

[4.5728]

[4.5828]

  uiStateRef.set {
    st with
      pendingCompletion := st.pendingCompletion.insert reqId (uri, row, col, query)
      latestCompletionReqId := some reqId
  }

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

B:BD[4.6741] → [2.4789:4856]

  uiStateRef.set { st with pendingCompletion := Lean.RBMap.empty }

[4.6741]

[4.6828]

  uiStateRef.set {
    st with
      pendingCompletion := Lean.RBMap.empty
      latestCompletionReqId := none
      completion := none
  }

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

B:BD[4.9341] → [4.9341:9386]

                let lspCol := cursor.col.val

[4.9341]

[2.5416]

                let lspCol := utf16ColFromDisplayCol lineStr state.config.tabStop cursor.col.val

Insertion in ViE/Lsp/Lean.lean at line 1196 [3.7243]
[3.30470]
[4.10471]
```
  if nextState.mode != .insert then
    clearUiCompletion
```
Replacement in Main.lean at line 48 [5.134883]
B:BD[5.136077] → [2.8105:8128]
```
  ViE.start config args
```
[5.136077]
```
  ViE.start config args
```

fix Lean completion LSP position to UTF-16 columns, ignore stale completion responses, and clear completion state on mode transitions

Dependencies

In channels

Change contents

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

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

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

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