s.foldl (fun acc c => acc + charWidth c) 0
/-- Calculate the total visual width of a substring. -/
def substringWidth (s : Substring.Raw) : Nat :=

/-- Count newlines in a byte array slice. -/
def countNewlines (data : ByteArray) (start : Nat) (len : Nat) : Nat :=
  let endPos := start + len
  let rec loop (i : Nat) (count : Nat) : Nat :=
    if i >= endPos then count
    else
      if data[i]! == 10 then loop (i + 1) (count + 1) -- 10 is \n
      else loop (i + 1) count
  loop start 0
/-- Count UTF-8 characters in a byte array range. -/
def countChars (bytes : ByteArray) (start len : Nat) : Nat :=
  let stop := start + len
  let rec loop (i : Nat) (cnt : Nat) : Nat :=
    if i >= stop then cnt
    else
      let b := bytes[i]!
      if (b &&& 0xC0) != 0x80 then
        loop (i + 1) (cnt + 1)
      else
        loop (i + 1) cnt
  loop start 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)]

/-- 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

/-- Calculate the total visual width of a substring with tab-stop awareness. -/
def substringWidthWithTabStop (s : Substring.Raw) (tabStop : Nat) : Nat :=
  let rec loop (i : String.Pos.Raw) (acc : Nat) : Nat :=
    if h : i.byteIdx < s.bsize then
      let c := s.get i
      let i' := s.next i
      have := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)
      let w := charWidthAt tabStop acc c
      loop i' (acc + w)
    else
      acc
    termination_by s.bsize - i.1
  loop 0 0

/-- Take characters from substring until visual width limit is reached. -/
def takeVisual (s : Substring.Raw) (width : Nat) : String :=
  Unicode.takeByDisplayWidth s width

def rightPadVisual (s : String) (width : Nat) : String :=
  let w := Unicode.stringWidth s
  if w >= width then
    s
  else
    s ++ "".pushn ' ' (width - w)

/-- Move cursor to specific row and column (0-indexed). -/
def moveCursor (row col : Nat) : IO Unit := do
  -- ANSI escape codes are 1-indexed.
  IO.print s!"\x1b[{row + 1};{col + 1}H"

/-- Hide cursor. -/
def hideCursor : IO Unit := do
  IO.print "\x1b[?25l"

/-- Show cursor. -/
def showCursor : IO Unit := do
  IO.print "\x1b[?25h"

def consumeWordBackward (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
  consumeWordBackwardCore tabStop buffer row col wantKw (wordMoveFuel buffer)

def consumeWordToEnd (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=
  consumeWordToEndCore tabStop buffer row col wantKw (wordMoveFuel buffer)

}
def initialWorkgroupState : WorkgroupState := {
  name := "1"
  workspaces := #[makeWorkspaceState defaultWorkspaceName none 0]
  currentWorkspace := 0

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

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

  ) #[]
private def asciiLowerChar (c : Char) : Char :=
  let n := c.toNat
  if 65 <= n && n <= 90 then
    Char.ofNat (n + 32)
  else
    c
private def asciiLower (s : String) : String :=
  String.map asciiLowerChar s
private def startsWithAt (s p : Array Char) (idx : Nat) : Bool :=
  if idx + p.size > s.size then
    false
  else
    Id.run do
      let mut ok := true
      for i in [0:p.size] do
        if s[idx + i]! != p[i]! then
          ok := false
      return ok
private def findSubseqMatch (q target : Array Char) : Option (Nat × Nat × Nat) :=
  if q.isEmpty then
    some (0, 0, 0)
  else
    Id.run do
      let mut qi := 0
      let mut start := 0
      let mut «end» := 0
      let mut foundStart := false
      for i in [0:target.size] do
        if qi < q.size && target[i]! == q[qi]! then
          if !foundStart then
            start := i
            foundStart := true
          qi := qi + 1
          if qi == q.size then
            «end» := i + 1
      if qi == q.size then
        let span := «end» - start
        some (start, «end», span)
      else
        none
private def scoreCompletion (query : String) (item : CompletionItem) : Int :=
  if query.isEmpty then
    0
  else
    let q := (asciiLower query).toList.toArray
    let tStr := asciiLower item.label
    let t := tStr.toList.toArray
    match findSubseqMatch q t with
    | none => -1000000
    | some (start, _, span) =>
        let isPrefix := startsWithAt t q 0
        let contiguous := span == q.size
        let prefixBonus : Int := if isPrefix then 1200 else 0
        let contiguousBonus : Int := if contiguous then 600 else 0
        let boundaryBonus : Int :=
          if start == 0 then
            200
          else
            let prev := t[start - 1]!
            if prev == '.' || prev == '_' || prev == ' ' then 120 else 0
        let gapPenalty : Int := Int.ofNat (span - q.size) * 8
        let lenPenalty : Int := Int.ofNat t.size
        prefixBonus + contiguousBonus + boundaryBonus - gapPenalty - lenPenalty
structure RankedCompletion where
  item : CompletionItem
  score : Int
  deriving Inhabited
private def betterRanked (a b : RankedCompletion) : Bool :=
  if a.score == b.score then
    a.item.label < b.item.label
  else
    a.score > b.score
private def heapSwap (arr : Array RankedCompletion) (i j : Nat) : Array RankedCompletion :=
  let ai := arr[i]!
  let aj := arr[j]!
  (arr.set! i aj).set! j ai
private def siftUp (heap : Array RankedCompletion) (idx : Nat) : Array RankedCompletion := Id.run do
  let mut h := heap
  let mut i := idx
  while i > 0 do
    let p := (i - 1) / 2
    if betterRanked h[p]! h[i]! then
      h := heapSwap h i p
      i := p
    else
      i := 0
  return h
private def siftDown (heap : Array RankedCompletion) (idx : Nat) : Array RankedCompletion := Id.run do
  let mut h := heap
  let mut i := idx
  let n := h.size
  let mut keep := true
  while keep do
    let l := 2 * i + 1
    if l >= n then
      keep := false
    else
      let r := l + 1
      let child :=
        if r < n && betterRanked h[l]! h[r]! then r else l
      if betterRanked h[i]! h[child]! then
        h := heapSwap h i child
        i := child
      else
        keep := false
  return h
private def heapPushTopK (heap : Array RankedCompletion) (k : Nat) (x : RankedCompletion) : Array RankedCompletion :=
  if k == 0 then
    #[]
  else if heap.size < k then
    siftUp (heap.push x) heap.size
  else if betterRanked x heap[0]! then
    siftDown (heap.set! 0 x) 0
  else
    heap
private def sortRankedDesc (arr : Array RankedCompletion) : Array RankedCompletion := Id.run do
  let mut out := arr
  let n := out.size
  for i in [1:n] do
    let cur := out[i]!
    let mut j := i
    while j > 0 && betterRanked cur out[j - 1]! do
      out := out.set! j out[j - 1]!
      j := j - 1
    out := out.set! j cur
  return out
private def rankAndSelectCompletions (query : String) (items : Array CompletionItem) (k : Nat := 40) : Array CompletionItem :=
  let heap := items.foldl (fun h item =>
    let sc := scoreCompletion query item
    if sc <= -1000000 then
      h
    else
      heapPushTopK h k { item := item, score := sc }

  let ranked := sortRankedDesc heap
  ranked.map (fun r => r.item)

  | some (uri, row, col) =>
      let items := parseCompletionItems result

  | some (uri, row, col, query) =>
      let items := rankAndSelectCompletions query (parseCompletionItems result) 40

          some (uri, { items := items.take 40, selected := 0, anchorRow := row, anchorCol := col })

          some (uri, { items := items, selected := 0, anchorRow := row, anchorCol := col })

private def requestCompletion (session : Session) (uri : String) (line lspCol row col : Nat) : IO Session := do

private def requestCompletion (session : Session) (uri : String) (line lspCol row col : Nat) (query : String) : IO Session := do

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

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

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

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

def acceptSelectedCompletion (state : EditorState) : IO EditorState := do
  clearUiCompletion
  pure (applySelectedCompletion state)

                clearUiCompletion

                let lineStr := ViE.getLineFromBuffer buf cursor.row |>.getD ""
                let startCol := completionPrefixStartDisplayCol lineStr state.config.tabStop cursor.col.val
                let startIdx := ViE.Unicode.displayColToCharIndexWithTabStop lineStr state.config.tabStop startCol
                let endIdx := ViE.Unicode.displayColToCharIndexWithTabStop lineStr state.config.tabStop cursor.col.val
                let chars := lineStr.toList
                let query := String.ofList (chars.drop startIdx |>.take (endIdx - startIdx))

                let s' ← requestCompletion s uri line lspCol cursor.row.val cursor.col.val

                let s' ← requestCompletion s uri line lspCol cursor.row.val cursor.col.val query

                pure { state with completionPopup := none }

                pure state
def acceptSelectedCompletion (state : EditorState) : IO EditorState := do
  clearUiCompletion
  let applied := applySelectedCompletion state
  if applied.mode == .insert then
    requestCompletionForActiveIfRunning applied
  else
    pure applied

  | none => pure { state with completionPopup := none }

  | none => pure state

      let matchesCursor := cursor.row.val == popup.anchorRow && cursor.col.val == popup.anchorCol
      if state.mode == .insert && matchesActive && matchesCursor then

      let sameLine := cursor.row.val == popup.anchorRow
      if state.mode == .insert && matchesActive && sameLine then

        pure { state with completionPopup := none }

        pure state

  let prevBuf := prevState.getActiveBuffer
  let nextBuf := nextState.getActiveBuffer
  let sameActiveBuffer := prevBuf.id == nextBuf.id
  let textChanged := sameActiveBuffer && prevBuf.table.toString != nextBuf.table.toString

  let cursorMoved :=
    let c0 := prevState.getCursor
    let c1 := nextState.getCursor
    c0.row != c1.row || c0.col != c1.col ||
      prevState.getActiveBuffer.id != nextState.getActiveBuffer.id

    if nextState.mode != .insert || cursorMoved then

    if nextState.mode != .insert then

  syncCompletionPopupFromUi infoSynced

  let completionRequested ←
    if infoSynced.mode == .insert && isLeanBuffer infoSynced.getActiveBuffer && textChanged then
      requestCompletionForActiveIfRunning infoSynced
    else
      pure infoSynced
  syncCompletionPopupFromUi completionRequested

import ViE.Lsp.Lean

import ViE.Language.Key

      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,

      do
        let handled ← ViE.Language.Key.handleInsertKey? s k
        match handled with
        | some s' => pure s'
        | none =>
            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 with completionPopup := none }
            | _ => pure s,

        left := mid
      else
        right := mid - 1
    return left
/-- Binary search to find child index containing the given line number -/
def findChildForLine (imeta : ViE.InternalMeta) (lineIdx : UInt64) : Nat :=
  Id.run do
    let arr := imeta.cumulativeLines
    if arr.isEmpty then return 0
    if arr.size == 1 then return 0
    let mut left := 0
    let mut right := arr.size - 2  -- Last valid child index
    while left < right do
      let mid := (left + right + 1) / 2
      if arr[mid]! <= lineIdx then

/-- Add a trigram to the Bloom filter. -/
def addTrigramToBloom (bloom : ByteArray) (b0 b1 b2 : UInt8) : ByteArray :=
  let h1 := hash1 b0 b1 b2
  let h2 := hash2 b0 b1 b2
  bloomSetBit (bloomSetBit bloom h1) h2

def bloomIsEmpty (bloom : ByteArray) : Bool :=
  bloom.data.all (fun b => b == 0)

def leafBloomBitsWithCache (pieces : Array ViE.Piece) (pt : ViE.PieceTable) (leafOffset : Nat)
  (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (maxSize : Nat)
  : (ByteArray × Lean.RBMap Nat ByteArray compare × Array Nat) :=
  match cache.find? leafOffset with
  | some bits => (bits, cache, order)
  | none =>
      let bits := (buildBloomForPieces pieces pt).bits
      let (cache', order') := cacheInsert cache order maxSize leafOffset bits
      (bits, cache', order')

/-- Flatten a tree into pieces in document order (iterative to avoid deep recursion). -/
def toPieces (t : ViE.PieceTree) : Array ViE.Piece := Id.run do
  let mut out : Array ViE.Piece := #[]
  let mut stack : List ViE.PieceTree := [t]
  while !stack.isEmpty do
    match stack with
    | [] => pure ()
    | node :: rest =>
        stack := rest
        match node with
        | ViE.PieceTree.empty => pure ()
        | ViE.PieceTree.leaf pieces _ _ =>
            out := out ++ pieces
        | ViE.PieceTree.internal children _ _ _ =>
            let mut i := children.size
            while i > 0 do
              let j := i - 1
              stack := children[j]! :: stack
              i := j
  return out

def replaceFirstInLine (line : String) (old : String) (new : String) : String :=
  if old.isEmpty then
    line
  else
    let parts := line.splitOn old
    match parts with
    | [] => line
    | p :: rest =>
        if rest.isEmpty then
          line
        else
          p ++ new ++ (String.intercalate old rest)
def replaceAllInLine (line : String) (old : String) (new : String) : String :=
  if old.isEmpty then
    line
  else
    String.intercalate new (line.splitOn old)

def loadPreviewBufferByteArray (filename : String) (maxBytes : Nat) : IO FileBuffer := do
  try
    let path := System.FilePath.mk filename
    if ← path.pathExists then
      if ← path.isDir then
        return emptyBuffer (some filename) true false
      else
        let data ← IO.FS.withFile filename IO.FS.Mode.read fun handle =>
          handle.read (USize.ofNat maxBytes)
        return bufferFromData filename data true false
    else
      return emptyBuffer (some filename) true false
  catch _ =>
    return emptyBuffer (some filename) true false

/-- Convert byte offset to Row/Col (display column) using default tab stop. -/
def getPointFromOffsetInBuffer (buffer : FileBuffer) (offset : Nat) : Point :=
  getPointFromOffsetInBufferWithTabStop buffer offset defaultConfig.tabStop

/-- Update FileBuffer from TextBuffer (compatibility function) -/
def fileBufferUpdateFromTextBuffer (buf : FileBuffer) (newContent : TextBuffer) : FileBuffer :=
  let newBuf := fileBufferFromTextBuffer buf.id buf.filename newContent
  { newBuf with dirty := true }

/-- Modify a line in FileBuffer using PieceTable operations -/
def modifyLineInBuffer (buffer : FileBuffer) (row : Row) (f : String → String) : FileBuffer :=
  match buffer.table.getLineRange row.val with
  | some (startOffset, length) =>
     match getLineFromBuffer buffer row with
     | some oldLine =>
        let newLine := f oldLine
        -- Edit: Delete old line content, insert new content.
        -- We preserve the newline character if it exists (getLineRange excludes it).
        let table' := buffer.table.delete startOffset length startOffset
        let table'' := table'.insert startOffset newLine startOffset
        { buffer with
          table := table''
          dirty := true
        }
     | none => buffer -- Should check range first, but safe fallback
  | none => buffer -- Line not found

/-- Empty buffer with one empty line -/
def emptyTextBuffer : TextBuffer :=
  #[#[]]

/-- Helper to update a specific line in the buffer. -/
def modifyLine (buffer : TextBuffer) (row : Row) (f : String → String) : TextBuffer :=
  if h : row.val < buffer.size then
    let oldLine := buffer[row.val]
    let newLine := stringToLine (f (lineToString oldLine))
    buffer.set! row.val newLine
  else
    buffer
/-- Set a line directly (String version for compatibility) -/
def setLine (buffer : TextBuffer) (row : Row) (content : String) : TextBuffer :=
  buffer.set! row.val (stringToLine content)
/-- Take first n elements from Array -/
def arrayTake {α : Type _} (arr : Array α) (n : Nat) : Array α :=
  arr.extract 0 n

/-- Drop first n elements from Array -/
def arrayDrop {α : Type _} (arr : Array α) (n : Nat) : Array α :=
  arr.extract n arr.size
/-- Concatenate multiple arrays -/
def arrayConcat {α : Type _} (arrays : List (Array α)) : Array α :=
  arrays.foldl (· ++ ·) #[]

/-- Insert a character at the cursor position. -/
def insertAtCursor (state : EditorState) (c : Char) : EditorState :=
  state.insertChar c

def testLeanCompletionPopupBehavior : IO Unit := do
  IO.println "  Testing Lean Completion Popup..."
  let popup : CompletionPopup := {
    items := #[
      { label := "foo", insertText := "foo" },
      { label := "foobar", insertText := "foobar" }
    ]
    selected := 0
    anchorRow := 0
    anchorCol := 2
  }
  let s0 : EditorState :=
    ({ ViE.initialState with mode := .insert, completionPopup := some popup }).updateActiveBuffer fun b =>
      { b with filename := some "Main.lean", table := ViE.PieceTable.fromString "ab" }
  let s0 := s0.setCursor { row := ⟨0⟩, col := ⟨2⟩ }

  let s1 ← runKeys s0 [Key.char 'c']
  assertBuffer "completion popup keeps showing on char insert" s1 "abc"
  assertEqual "completion popup remains visible after char insert" true s1.completionPopup.isSome
  let s2 ← runKeys s1 [Key.enter]
  assertBuffer "Enter inserts newline instead of accepting completion" s2 "abc\n"
  assertCursor "Enter moves cursor to next line head with completion popup" s2 1 0
  assertEqual "Enter closes completion popup" true s2.completionPopup.isNone

  testLeanCompletionPopupBehavior

  ViE.start config args

  ViE.start config args