let activeCursorPos := getCursorPos (baseLayout.getD wsAfterLayout.layout) 0 0 layoutH cols
  buffer := buffer ++ renderCompletionPopup rows cols stateAfterLayout activeCursorPos

      match getCursorPos (baseLayout.getD wsAfterLayout.layout) 0 0 layoutH cols with

      match activeCursorPos with

private def repeatStr (s : String) (n : Nat) : String :=
  Id.run do
    let mut out := ""
    for _ in [0:n] do
      out := out ++ s
    return out
def renderCompletionPopup (rows cols : Nat) (state : EditorState) (cursorPos : Option (Nat × Nat)) : Array String := Id.run do
  let some popup := state.completionPopup | return #[]
  let some (cursorRow, cursorCol) := cursorPos | return #[]
  if popup.items.isEmpty then
    return #[]
  let availableRows := if rows > 1 then rows - 1 else rows
  if availableRows < 4 || cols < 8 then
    return #[]
  let visibleMax := min 8 popup.items.size
  let labels := popup.items.extract 0 visibleMax |>.map (fun it => it.label)
  let naturalW := labels.foldl (fun acc s => max acc (ViE.Unicode.stringWidthWithTabStop s state.config.tabStop)) 0
  let innerWidth := max 8 (min 48 naturalW)
  let boxWidth := innerWidth + 2
  let boxHeight := visibleMax + 2
  let placeBelow := cursorRow + 1 + boxHeight <= availableRows
  let top :=
    if placeBelow then
      cursorRow + 1
    else if cursorRow >= boxHeight then
      cursorRow - boxHeight
    else
      0
  let left0 := cursorCol
  let left := if left0 + boxWidth < cols then left0 else cols - boxWidth
  let hline := repeatStr state.config.hSplitStr innerWidth
  let borderTop := state.config.vSplitStr ++ hline ++ state.config.vSplitStr
  let borderBottom := borderTop
  let mut out : Array String := #[]
  out := out.push (Terminal.moveCursorStr top left)
  out := out.push borderTop
  let selected := if popup.selected < visibleMax then popup.selected else 0
  for i in [0:visibleMax] do
    let label := labels[i]!
    let clipped := ViE.Unicode.takeByDisplayWidthWithTabStop label.toRawSubstring state.config.tabStop innerWidth
    let clippedW := ViE.Unicode.stringWidthWithTabStop clipped state.config.tabStop
    let pad := if clippedW < innerWidth then "".pushn ' ' (innerWidth - clippedW) else ""
    let row := top + 1 + i
    out := out.push (Terminal.moveCursorStr row left)
    out := out.push state.config.vSplitStr
    if i == selected then
      out := out.push state.config.searchHighlightCursorStyle
      out := out.push clipped
      out := out.push pad
      out := out.push state.config.resetStyle
    else
      out := out.push clipped
      out := out.push pad
    out := out.push state.config.vSplitStr
  out := out.push (Terminal.moveCursorStr (top + boxHeight - 1) left)
  out := out.push borderBottom
  return out

structure CompletionItem where
  label : String
  insertText : String
  deriving Repr, Inhabited
structure CompletionPopup where
  items : Array CompletionItem
  selected : Nat := 0
  anchorRow : Nat
  anchorCol : Nat
  deriving Repr, Inhabited

  completionPopup : Option CompletionPopup := none

  completionPopup := none

import ViE.Unicode

  pendingCompletion : Lean.RBMap Nat (String × Nat × Nat) compare

  completion : Option (String × CompletionPopup)

    pendingCompletion := Lean.RBMap.empty

    completion := none

    pendingCompletion := Lean.RBMap.empty

    completion := none

private def parseCompletionItem (j : Lean.Json) : Option CompletionItem := do
  let label ← getObjStr? j "label"
  let insertText :=
    (getObjStr? j "insertText").getD <|
      match (j.getObjVal? "textEdit").toOption with
      | some te => (getObjStr? te "newText").getD label
      | none => label
  some { label := label, insertText := insertText }

private def parseCompletionItems (result : Lean.Json) : Array CompletionItem :=
  let rawItems : Array Lean.Json :=
    match result with
    | .arr xs => xs
    | .obj _ => (result.getObjValAs? (Array Lean.Json) "items").toOption.getD #[]
    | _ => #[]
  rawItems.foldl (fun acc j =>
    match parseCompletionItem j with
    | some item =>
        if item.insertText.isEmpty then acc else acc.push item
    | none => acc
  ) #[]

private def handleCompletionResponse (reqId : Nat) (result : Lean.Json) : IO Unit := do
  let st ← uiStateRef.get
  let pending := st.pendingCompletion
  let pending' := pending.erase reqId
  match pending.find? reqId with
  | none =>
      uiStateRef.set { st with pendingCompletion := pending' }
  | some (uri, row, col) =>
      let items := parseCompletionItems result
      let completion :=
        if items.isEmpty then
          none
        else
          some (uri, { items := items.take 40, selected := 0, anchorRow := row, anchorCol := col })
      uiStateRef.set { st with pendingCompletion := pending', completion := completion }

          handleHoverResponse reqId result

          let st ← uiStateRef.get
          if st.pendingHover.find? reqId |>.isSome then
            handleHoverResponse reqId result
          else if st.pendingCompletion.find? reqId |>.isSome then
            handleCompletionResponse reqId result
          else
            pure ()

            uiStateRef.set { st with pendingHover := st.pendingHover.erase reqId }

            uiStateRef.set {
              st with
                pendingHover := st.pendingHover.erase reqId
                pendingCompletion := st.pendingCompletion.erase reqId
            }

private def requestCompletion (session : Session) (uri : String) (line lspCol row col : Nat) : IO Session := do
  let reqId := session.nextId
  let params := Lean.Json.mkObj [
    ("textDocument", Lean.Json.mkObj [("uri", .str uri)]),
    ("position", Lean.Json.mkObj [
      ("line", (line : Lean.Json)),
      ("character", (lspCol : Lean.Json))
    ]),
    ("context", Lean.Json.mkObj [("triggerKind", (1 : Lean.Json))])
  ]
  send session.child.stdin (mkRequest reqId "textDocument/completion" params)
  let st ← uiStateRef.get
  uiStateRef.set { st with pendingCompletion := st.pendingCompletion.insert reqId (uri, row, col) }
  pure { session with nextId := reqId + 1 }

private def completionIdentChar (c : Char) : Bool :=
  c.isAlphanum || c == '_' || c == '\''
private def completionPrefixStartDisplayCol (line : String) (tabStop cursorCol : Nat) : Nat :=
  let charIdx := ViE.Unicode.displayColToCharIndexWithTabStop line tabStop cursorCol
  let prefixChars : Array Char := (line.toList.take charIdx).toArray
  let startIdx := Id.run do
    let mut i := prefixChars.size
    while i > 0 do
      let j := i - 1
      let c := prefixChars[j]!
      if completionIdentChar c then
        i := j
      else
        return i
    return 0
  let before := String.ofList (prefixChars.toList.take startIdx)
  ViE.Unicode.stringWidthWithTabStop before tabStop
def clearCompletionPopup (state : EditorState) : EditorState :=
  { state with completionPopup := none }
private def clearUiCompletion : IO Unit := do
  let st ← uiStateRef.get
  uiStateRef.set { st with completion := none, pendingCompletion := Lean.RBMap.empty }
def selectNextCompletion (state : EditorState) : EditorState :=
  match state.completionPopup with
  | none => state
  | some popup =>
      if popup.items.isEmpty then
        { state with completionPopup := none }
      else
        let next := (popup.selected + 1) % popup.items.size
        { state with completionPopup := some { popup with selected := next } }
def selectPrevCompletion (state : EditorState) : EditorState :=
  match state.completionPopup with
  | none => state
  | some popup =>
      if popup.items.isEmpty then
        { state with completionPopup := none }
      else
        let prev := if popup.selected == 0 then popup.items.size - 1 else popup.selected - 1
        { state with completionPopup := some { popup with selected := prev } }

private def applySelectedCompletion (state : EditorState) : EditorState :=
  match state.completionPopup with
  | none => state
  | some popup =>
      if popup.items.isEmpty || popup.selected >= popup.items.size then
        { state with completionPopup := none }
      else
        let item := popup.items[popup.selected]!
        let cursor := state.getCursor
        let line := ViE.getLineFromBuffer state.getActiveBuffer cursor.row |>.getD ""
        let startCol := completionPrefixStartDisplayCol line state.config.tabStop cursor.col.val
        let deleteCount := cursor.col.val - startCol
        let sDeleted := Id.run do
          let mut s := state
          for _ in [0:deleteCount] do
            s := s.deleteBeforeCursor
          return s
        let sInserted := Id.run do
          let mut s := sDeleted
          for c in item.insertText.toList do
            s := s.insertChar c
          return s
        { sInserted with completionPopup := none }
def acceptSelectedCompletion (state : EditorState) : IO EditorState := do
  clearUiCompletion
  pure (applySelectedCompletion state)
def requestCompletionForActiveIfRunning (state : EditorState) : IO EditorState := do
  let buf := state.getActiveBuffer
  let cursor := state.getCursor
  match buf.filename with
  | none => pure state
  | some path =>
      if !isLeanPath path then
        pure state
      else
        match (← sessionRef.get) with
        | none => pure state
        | some s =>
            match (← s.child.tryWait) with
            | some _ =>
                sessionRef.set none
                pure state
            | none =>
                clearUiCompletion
                let uri := fileUri path
                let line := cursor.row.val
                let lspCol := cursor.col.val
                let s' ← requestCompletion s uri line lspCol cursor.row.val cursor.col.val
                sessionRef.set (some s')
                pure { state with completionPopup := none }
private def syncCompletionPopupFromUi (state : EditorState) : IO EditorState := do
  let st ← uiStateRef.get
  match st.completion with
  | none => pure { state with completionPopup := none }
  | some (uri, popup) =>
      let matchesActive :=
        match state.getActiveBuffer.filename with
        | some path => fileUri path == uri
        | none => false
      let cursor := state.getCursor
      let matchesCursor := cursor.row.val == popup.anchorRow && cursor.col.val == popup.anchorCol
      if state.mode == .insert && matchesActive && matchesCursor then
        pure { state with completionPopup := some popup }
      else
        pure { state with completionPopup := none }

  syncInfoViewWindow nextState

  let cursorMoved :=
    let c0 := prevState.getCursor
    let c1 := nextState.getCursor
    c0.row != c1.row || c0.col != c1.col ||
      prevState.getActiveBuffer.id != nextState.getActiveBuffer.id
  let noCompletion :=
    if nextState.mode != .insert || cursorMoved then
      clearCompletionPopup nextState
    else
      nextState
  let infoSynced ← syncInfoViewWindow noCompletion
  syncCompletionPopupFromUi infoSynced

import ViE.Lsp.Lean

      match k with
      | Key.esc => pure $ (s.commitEdit.moveCursorLeft).setMode Mode.normal
      | Key.backspace => pure $ s.deleteBeforeCursor
      | Key.char c => pure $ s.insertChar c
      | Key.enter => pure s.insertNewline
      | _ => pure s,

      match s.completionPopup with
      | some _ =>
          match k with
          | Key.ctrl 'n' | Key.down => pure <| ViE.Lsp.Lean.selectNextCompletion s
          | Key.ctrl 'p' | Key.up => pure <| ViE.Lsp.Lean.selectPrevCompletion s
          | Key.enter | Key.char '\t' => ViE.Lsp.Lean.acceptSelectedCompletion s
          | Key.esc => pure <| ViE.Lsp.Lean.clearCompletionPopup ((s.commitEdit.moveCursorLeft).setMode Mode.normal)
          | Key.backspace => pure <| ViE.Lsp.Lean.clearCompletionPopup (s.deleteBeforeCursor)
          | Key.char c => pure <| ViE.Lsp.Lean.clearCompletionPopup (s.insertChar c)
          | _ => pure <| ViE.Lsp.Lean.clearCompletionPopup s
      | none =>
          match k with
          | Key.ctrl 'n' => ViE.Lsp.Lean.requestCompletionForActiveIfRunning s
          | Key.esc => pure $ (s.commitEdit.moveCursorLeft).setMode Mode.normal
          | Key.backspace => pure $ s.deleteBeforeCursor
          | Key.char c => pure $ s.insertChar c
          | Key.enter => pure s.insertNewline
          | _ => pure s,