editSessionId : Nat := 0

  diagnostics : Lean.RBMap String (Array DiagnosticInfo) compare

    diagnostics := Lean.RBMap.empty

private def diagnosticsShardCount : Nat := 16
private abbrev DiagnosticsMap := Lean.RBMap String (Array DiagnosticInfo) compare
initialize diagnosticsShards : Array (IO.Ref DiagnosticsMap) ← do
  let mut shards : Array (IO.Ref DiagnosticsMap) := #[]
  for _ in [0:diagnosticsShardCount] do
    let r ← IO.mkRef (Lean.RBMap.empty : DiagnosticsMap)
    shards := shards.push r
  pure shards

private def diagnosticsShardIdx (uri : String) : Nat :=
  (hash uri).toNat % diagnosticsShardCount
private def diagnosticsGet (uri : String) : IO (Array DiagnosticInfo) := do
  let idx := diagnosticsShardIdx uri
  match diagnosticsShards[idx]? with
  | none => pure #[]
  | some shard =>
      let m ← shard.get
      pure ((m.find? uri).getD #[])
private def diagnosticsInsert (uri : String) (items : Array DiagnosticInfo) : IO Unit := do
  let idx := diagnosticsShardIdx uri
  match diagnosticsShards[idx]? with
  | none => pure ()
  | some shard =>
      shard.modify fun m => m.insert uri items
private def diagnosticsClearAll : IO Unit := do
  for shard in diagnosticsShards do
    shard.set (Lean.RBMap.empty : DiagnosticsMap)

    diagnostics := Lean.RBMap.empty
  }

  } *> diagnosticsClearAll

    let st ← uiStateRef.get
    uiStateRef.set { st with diagnostics := st.diagnostics.insert uri parsed }

    diagnosticsInsert uri parsed

  let st ← uiStateRef.get
  let pending := st.pendingHover
  let hoverMap := pending.erase reqId
  match pending.find? reqId with
  | none =>
      uiStateRef.set { st with pendingHover := hoverMap }
  | some (uri, line, col) =>
      let hover :=
        match parseHoverText result with
        | some txt =>
            let range? := parseHoverRange result
            some { uri := uri, line := line, col := col, range? := range?, text := txt }
        | none =>
            match st.hover with
            | some h =>
                if h.uri == uri && h.line == line && h.col == col then some h else none
            | none => none
      uiStateRef.set { st with pendingHover := hoverMap, hover := hover }

  uiStateRef.modify fun st =>
    let pending := st.pendingHover
    let hoverMap := pending.erase reqId
    match pending.find? reqId with
    | none =>
        { st with pendingHover := hoverMap }
    | some (uri, line, col) =>
        let hover :=
          match parseHoverText result with
          | some txt =>
              let range? := parseHoverRange result
              some { uri := uri, line := line, col := col, range? := range?, text := txt }
          | none =>
              match st.hover with
              | some h =>
                  if h.uri == uri && h.line == line && h.col == col then some h else none
              | none => none
        { st with pendingHover := hoverMap, hover := hover }

  let st ← uiStateRef.get
  let pending := st.pendingCompletion
  let pending' := pending.erase reqId
  let isLatest := st.latestCompletionReqId == some reqId
  match pending.find? reqId with
  | none =>
      uiStateRef.set { st with pendingCompletion := pending' }
  | some (uri, row, col, query) =>
      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
        }

  uiStateRef.modify fun st =>
    let pending := st.pendingCompletion
    let pending' := pending.erase reqId
    let isLatest := st.latestCompletionReqId == some reqId
    match pending.find? reqId with
    | none =>
        { st with pendingCompletion := pending' }
    | some (uri, row, col, query) =>
        if !isLatest then
          { 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 })
          {
            st with
              pendingCompletion := pending'
              latestCompletionReqId := none
              completion := completion
          }

            let st ← uiStateRef.get
            let clearCompletion := st.latestCompletionReqId == some reqId
            uiStateRef.set {
              st with
                pendingHover := st.pendingHover.erase reqId
                pendingCompletion := st.pendingCompletion.erase reqId
                latestCompletionReqId := if clearCompletion then none else st.latestCompletionReqId
                completion := if clearCompletion then none else st.completion
            }

            uiStateRef.modify fun st =>
              let clearCompletion := st.latestCompletionReqId == some reqId
              {
                st with
                  pendingHover := st.pendingHover.erase reqId
                  pendingCompletion := st.pendingCompletion.erase reqId
                  latestCompletionReqId := if clearCompletion then none else st.latestCompletionReqId
                  completion := if clearCompletion then none else st.completion
              }

            match (← initializeAckRef.get) with

            let got? ← initializeAckRef.modifyGet fun got =>
              (got, none)
            match got? with

                initializeAckRef.set none

        let text := buf.table.toString

        let text ← ViE.PieceTree.getSubstringParallelIO buf.table.tree 0 buf.table.tree.length buf.table

  let st ← uiStateRef.get
  uiStateRef.set { st with pendingHover := st.pendingHover.insert reqId (uri, line, cursorCol) }

  uiStateRef.modify fun st =>
    { st with pendingHover := st.pendingHover.insert reqId (uri, line, cursorCol) }

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

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

  let st ← uiStateRef.get
  uiStateRef.set {
    st with

  uiStateRef.modify fun st =>
    {
      st with

  }

    }

  let problems := st.diagnostics.find? uri |>.getD #[]

  let problems ← diagnosticsGet uri

  let textChanged := sameActiveBuffer && prevBuf.table.toString != nextBuf.table.toString

  let textChanged := sameActiveBuffer && prevBuf.table.contentVersion != nextBuf.table.contentVersion

        oldBuf.table.toString != newBuf.table.toString

        oldBuf.table.contentVersion != newBuf.table.contentVersion

import ViE.Buffer.EditQueue

          return some <| ViE.Lsp.Lean.clearCompletionPopup ((state.commitEdit.moveCursorLeft).setMode Mode.normal)

          let s' ← ViE.Buffer.EditQueue.awaitActiveInsertOps state
          return some <| ViE.Lsp.Lean.clearCompletionPopup ((s'.commitEdit.moveCursorLeft).setMode Mode.normal)

          let s' := state.deleteBeforeCursor

          let s1 ← ViE.Buffer.EditQueue.awaitActiveInsertOps state
          let s' := s1.deleteBeforeCursor

          let s' := state.deleteBeforeCursor

          let s1 ← ViE.Buffer.EditQueue.awaitActiveInsertOps state
          let s' := s1.deleteBeforeCursor

import ViE.Buffer.EditQueue

  normal := fun s k =>

  normal := fun s k => do
  let s ← ViE.Buffer.EditQueue.awaitActiveInsertOps s

            pure $ clearInput (EditorState.jumpToLine s line)

            pure $ clearInput ((EditorState.jumpToLine s line).moveToLineStart)

            pure $ clearInput (EditorState.jumpToLine s line)

            pure $ clearInput ((EditorState.jumpToLine s line).moveToLineStart)

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

            | Key.esc => do
                let s' ← ViE.Buffer.EditQueue.awaitActiveInsertOps s
                pure $ (s'.commitEdit.moveCursorLeft).setMode Mode.normal
            | Key.backspace => do
                let s' ← ViE.Buffer.EditQueue.enqueueBackspace s
                ViE.Buffer.EditQueue.awaitActiveInsertOps s'
            | Key.char c => ViE.Buffer.EditQueue.enqueueInsertChar s c
            | Key.enter => do
                let s' ← ViE.Buffer.EditQueue.enqueueInsertNewline s
                let s'' ← ViE.Buffer.EditQueue.awaitActiveInsertOps s'
                pure { s'' with completionPopup := none }

        pure $ clearInput (EditorState.jumpToLine s line)

        pure $ clearInput ((EditorState.jumpToLine s line).moveToLineStart)

               pure $ clearInput (EditorState.jumpToLine s line)

               pure $ clearInput ((EditorState.jumpToLine s line).moveToLineStart)

        pure $ clearInput (EditorState.jumpToLine s line)

        pure $ clearInput ((EditorState.jumpToLine s line).moveToLineStart)

               pure $ clearInput (EditorState.jumpToLine s line)

               pure $ clearInput ((EditorState.jumpToLine s line).moveToLineStart)

    -- File contents changed on disk; drop read cache for this path.
    ViE.invalidateBufferLoadCache filename

/-- Build line-start offsets by walking the piece tree in document order. -/
private def buildLineIndex (pt : PieceTable) : Array Nat := Id.run do
  let capacity := PieceTree.lineBreaks pt.tree + 1
  let mut starts : Array Nat := (Array.mkEmpty capacity).push 0
  let mut docOff := 0
  let mut stack : List PieceTree := [pt.tree]
  while !stack.isEmpty do
    match stack with
    | [] => pure ()
    | node :: rest =>
        stack := rest
        match node with
        | PieceTree.empty => pure ()
        | PieceTree.leaf pieces _ _ =>
            for p in pieces do
              let buf := PieceTableHelper.getBuffer pt p.source
              let stop := p.start.toNat + p.length.toNat
              let mut i := p.start.toNat
              while i < stop do
                if buf[i]! == 10 then
                  starts := starts.push (docOff + 1)
                i := i + 1
                docOff := docOff + 1
        | PieceTree.internal children _ _ _ =>
            let mut i := children.size
            while i > 0 do
              let j := i - 1
              stack := children[j]! :: stack
              i := j
  return starts

private def updateLineIndexOnInsert (_pt : PieceTable) (_offset : Nat) (_text : String) : Option (Array Nat) :=
  none

private def withLineIndexCache (pt : PieceTable) : PieceTable :=
  { pt with lineIndexCache := some (buildLineIndex pt) }

private def updateLineIndexOnDelete (_pt : PieceTable) (_offset : Nat) (_length : Nat) : Option (Array Nat) :=
  none

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none, lineIndexCache := some #[0]

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none, lineIndexCache := none

    -- Split bytes into chunks while collecting line starts in one pass.
    let rec splitChunks (start : Nat) (pieces : Array Piece) (starts : Array Nat) : (Array Piece × Array Nat) :=

    -- Split bytes into chunks.
    let rec splitChunks (start : Nat) (pieces : Array Piece) : Array Piece :=

        (pieces, starts)

        pieces

        let rec scan (i : Nat) (lines chars : Nat) (lineStarts : Array Nat) : (Nat × Nat × Array Nat) :=

        let rec scan (i : Nat) (lines chars : Nat) : (Nat × Nat) :=

            (lines, chars, lineStarts)

            (lines, chars)

            let lineStarts' := if b == 10 then lineStarts.push (i + 1) else lineStarts

            scan (i + 1) lines' chars' lineStarts'
        let (lines, chars, starts') := scan start 0 0 starts

            scan (i + 1) lines' chars'
        let (lines, chars) := scan start 0 0

        splitChunks (start + len) (pieces.push piece) starts'

        splitChunks (start + len) (pieces.push piece)

    let (pieces, starts) := splitChunks 0 #[] #[0]

    let pieces := splitChunks 0 #[]

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none, lineIndexCache := some starts

      undoStack := [], redoStack := [], undoLimit := 100, lastInsert := none, lineIndexCache := none

private def PieceTable.lineIndex (pt : PieceTable) : Array Nat :=
  match pt.lineIndexCache with
  | some idx => idx
  | none => buildLineIndex pt

    withLineIndexCache { pt' with

    { pt' with

      contentVersion := pt.contentVersion + 1
      lineIndexCache := updateLineIndexOnInsert pt offset text

    withLineIndexCache { pt with

    { pt with

      contentVersion := pt.contentVersion + 1
      lineIndexCache := updateLineIndexOnDelete pt offset length

    { pt' with tree := newTree, lineIndexCache := none, lastInsert := none }

    { pt' with
      tree := newTree
      contentVersion := pt.contentVersion + 1
      lineIndexCache := updateLineIndexOnInsert pt offset text
      lastInsert := none
    }

    { pt with tree := newTree, lineIndexCache := none, lastInsert := none }

    { pt with
      tree := newTree
      contentVersion := pt.contentVersion + 1
      lineIndexCache := updateLineIndexOnDelete pt offset length
      lastInsert := none
    }

    withLineIndexCache { pt' with

    { pt' with

    (withLineIndexCache { pt with

    ({ pt with

      contentVersion := pt.contentVersion + 1
      lineIndexCache := none

    (withLineIndexCache { pt with

    ({ pt with

      contentVersion := pt.contentVersion + 1
      lineIndexCache := none

  let idx := pt.lineIndex
  match idx[lineIdx]? with
  | none => none
  | some startOff =>
      let totalLen := pt.tree.length
      match idx[lineIdx + 1]? with
      | some nextStart =>
          let len := if nextStart > startOff then (nextStart - startOff - 1) else 0
          some (startOff, len)
      | none =>
          some (startOff, totalLen - startOff)

  PieceTree.getLineRange pt.tree lineIdx pt

private def PieceTable.findLineForOffsetCore (pt : PieceTable) (target : Nat) (low highExcl : Nat) : Option (Nat × Nat) :=
  if low >= highExcl then none
  else
    let mid := low + (highExcl - low) / 2
    match pt.getLineRange mid with
    | some (start, len) =>
      let endOff := start + len
      if target >= start && target <= endOff then
        some (mid, target - start)
      else if target < start then
        PieceTable.findLineForOffsetCore pt target low mid
      else
        PieceTable.findLineForOffsetCore pt target (mid + 1) highExcl
    | none => none
  termination_by highExcl - low
  decreasing_by
    · simp_wf
      omega
    · simp_wf
      omega
def PieceTable.findLineForOffset (pt : PieceTable) (target : Nat) (low high : Nat) : Option (Nat × Nat) :=
  PieceTable.findLineForOffsetCore pt target low (high + 1)

  let hi := pt.lineCount - 1
  match PieceTable.findLineForOffset pt offset 0 hi with
  | some (r, c) =>
    match PieceTable.getLineRange pt r with
    | some (startOff, len) =>
      let rel := if c <= len then c else len

  let clamped := min offset pt.length
  let r := PieceTree.getLineIndexAtOffset pt.tree clamped pt
  match PieceTable.getLineRange pt r with
  | some (startOff, len) =>
      let rel0 := if clamped >= startOff then clamped - startOff else 0
      let rel := min rel0 len

    | none => (r, c)
  | none => (0, 0) -- Fallback

  | none => (0, 0)

        left := mid
      else
        right := mid - 1
    return left
/-- Binary search to find child index containing the given line-break index. -/
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
    while left < right do
      let mid := (left + right + 1) / 2
      if arr[mid]! <= lineIdx then

/-- Parallel byte extraction for large ranges. Falls back to `getBytes` for small reads. -/
def getBytesParallelIO (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable)
  (chunkSize : Nat := 128 * 1024) (parallelChunks : Nat := 4) : IO ByteArray := do
  if len == 0 || parallelChunks <= 1 || len <= chunkSize then
    pure (getBytes t offset len pt)
  else
    let chunks : Array (Nat × Nat) := Id.run do
      let mut out : Array (Nat × Nat) := #[]
      let mut off := offset
      let endOff := offset + len
      while off < endOff do
        let readLen := min chunkSize (endOff - off)
        out := out.push (off, readLen)
        off := off + readLen
      return out
    if chunks.size <= 1 then
      pure (getBytes t offset len pt)
    else
      let mut out : ByteArray := ByteArray.mk (Array.mkEmpty len)
      let mut i := 0
      while i < chunks.size do
        let mut batch : Array (Task (Except IO.Error ByteArray)) := #[]
        let mut j := 0
        while j < parallelChunks && i + j < chunks.size do
          let (off, l) := chunks[i + j]!
          let task ← IO.asTask (pure (getBytes t off l pt))
          batch := batch.push task
          j := j + 1
        for task in batch do
          match task.get with
          | .ok part =>
              for b in part.data do
                out := out.push b
          | .error e => throw e
        i := i + batch.size
      pure out

/-- Parallel substring extraction for large ranges. -/
def getSubstringParallelIO (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable)
  (chunkSize : Nat := 128 * 1024) (parallelChunks : Nat := 4) : IO String := do
  let bytes ← getBytesParallelIO t offset len pt chunkSize parallelChunks
  pure (String.fromUTF8! bytes)

      | ViE.PieceTree.internal children _ _ _ =>
          let mut i := 0
          let mut found := false
          while i < children.size && !found do
            let child := children[i]!
            let childLines := lineBreaks child
            if currN < childLines then
              node := child
              found := true
            else
              currN := currN - childLines
              currOff := currOff + length child
              i := i + 1
          if !found then

      | ViE.PieceTree.internal children _ _ imeta =>
          if children.isEmpty then

          let childIdx := findChildForLine imeta currN.toUInt64
          let child := children[childIdx]!
          currN := currN - imeta.cumulativeLines[childIdx]!.toNat
          currOff := currOff + imeta.cumulativeBytes[childIdx]!.toNat
          node := child

/-- Get line index (0-based) containing the byte offset.
    Newline byte itself belongs to the previous line (same as getLineRange semantics). -/
def getLineIndexAtOffset (t : ViE.PieceTree) (offset : Nat) (pt : ViE.PieceTable) : Nat := Id.run do
  let target := min offset (length t)
  let mut node := t
  let mut currLines := 0
  let mut rem := target
  while true do
    match node with
    | ViE.PieceTree.empty =>
        return currLines
    | ViE.PieceTree.leaf pieces _ _ =>
        let mut i := 0
        while i < pieces.size && rem > 0 do
          let p := pieces[i]!
          let pLen := p.length.toNat
          if rem >= pLen then
            currLines := currLines + p.lineBreaks.toNat
            rem := rem - pLen
          else
            let buf := PieceTableHelper.getBuffer pt p.source
            let (lines, _) := ViE.Unicode.countNewlinesAndChars buf p.start.toNat rem
            currLines := currLines + lines
            rem := 0
          i := i + 1
        return currLines
    | ViE.PieceTree.internal children _ _ imeta =>
        if children.isEmpty then
          return currLines
        let childIdx := findChildForOffset imeta rem.toUInt64
        currLines := currLines + imeta.cumulativeLines[childIdx]!.toNat
        let childStart := imeta.cumulativeBytes[childIdx]!.toNat
        rem := rem - childStart
        node := children[childIdx]!
  return currLines

  contentVersion : Nat := 0

import ViE.Buffer.EditQueue

  let state ← ViE.Buffer.EditQueue.ensureSessionId state

import ViE.Buffer.EditQueue

private def loadCacheShardCount : Nat := 16
private abbrev LoadCacheMap := Lean.RBMap String FileBuffer compare
initialize loadCacheShards : Array (IO.Ref LoadCacheMap) ← do
  let mut shards : Array (IO.Ref LoadCacheMap) := #[]
  for _ in [0:loadCacheShardCount] do
    let r ← IO.mkRef (Lean.RBMap.empty : LoadCacheMap)
    shards := shards.push r
  pure shards
private def loadCacheKey (filename : String) (buildLeafBits buildOnEdit : Bool) : String :=
  s!"{filename}#bits={if buildLeafBits then "1" else "0"}#edit={if buildOnEdit then "1" else "0"}"
private def loadCacheShardIdx (key : String) : Nat :=
  (hash key).toNat % loadCacheShardCount
private def loadCacheGet (key : String) : IO (Option FileBuffer) := do
  let idx := loadCacheShardIdx key
  match loadCacheShards[idx]? with
  | none => pure none
  | some shard =>
      let m ← shard.get
      pure (m.find? key)
private def loadCacheInsert (key : String) (buf : FileBuffer) : IO Unit := do
  let idx := loadCacheShardIdx key
  match loadCacheShards[idx]? with
  | none => pure ()
  | some shard =>
      shard.modify fun m => m.insert key buf

private def loadCacheErase (key : String) : IO Unit := do
  let idx := loadCacheShardIdx key
  match loadCacheShards[idx]? with
  | none => pure ()
  | some shard =>
      shard.modify fun m => m.erase key

def invalidateBufferLoadCache (filename : String) : IO Unit := do
  for bits in [false, true] do
    for onEdit in [false, true] do
      loadCacheErase (loadCacheKey filename bits onEdit)

  let key := loadCacheKey filename buildLeafBits buildOnEdit

        let data ← IO.FS.readBinFile filename
        return bufferFromData filename data buildLeafBits buildOnEdit

        match (← loadCacheGet key) with
        | some cached => return cached
        | none =>
            let data ← IO.FS.readBinFile filename
            let buf := bufferFromData filename data buildLeafBits buildOnEdit
            loadCacheInsert key buf
            return buf

def prefetchBufferByteArrayWithConfig (filename : String) (config : EditorConfig) : IO Unit := do
  let _ ← IO.asTask do
    let _ ← loadBufferByteArrayWithConfig filename config
    pure ()
  pure ()

import ViE.State
import ViE.Unicode
namespace ViE.Buffer.EditQueue
open ViE
inductive InsertOp where
  | char (c : Char)
  | newline
  | backspace
  deriving Inhabited
structure WorkerState where
  buffer : FileBuffer
  cursor : Point
  tabStop : Nat
  deriving Inhabited
structure WorkerKey where
  sessionId : Nat
  bufferId : Nat
  deriving Repr, BEq, Ord, Inhabited
structure WorkerEntry where
  baseSig : UInt64
  submitted : Nat
  applied : Nat
  task : Task (Except IO.Error WorkerState)
private def bufferSig (b : FileBuffer) : UInt64 :=
  mixHash (hash b.table.tree.length) (hash b.table.tree.lineBreaks)
initialize workersRef : IO.Ref (Lean.RBMap WorkerKey WorkerEntry compare) ←
  IO.mkRef Lean.RBMap.empty
initialize sessionCounterRef : IO.Ref Nat ← IO.mkRef 1
def ensureSessionId (s : EditorState) : IO EditorState := do
  if s.editSessionId != 0 then
    pure s
  else
    let sid ← sessionCounterRef.modifyGet fun n => (n, n + 1)
    pure { s with editSessionId := sid }
private def applyInsertOp (ws : WorkerState) (op : InsertOp) : WorkerState :=
  match op with
  | .char c =>
      match ViE.getOffsetFromPointInBufferWithTabStop ws.buffer ws.cursor.row ws.cursor.col ws.tabStop with
      | none => ws
      | some offset =>
          let b' := { ws.buffer with table := ws.buffer.table.insert offset (c.toString) offset, dirty := true }
          let b'' := FileBuffer.clearCache (FileBuffer.recomputeMissingEol b')
          let delta := ViE.Unicode.charWidthAt ws.tabStop ws.cursor.col.val c
          { ws with buffer := b'', cursor := { ws.cursor with col := ⟨ws.cursor.col.val + delta⟩ } }
  | .newline =>
      match ViE.getOffsetFromPointInBufferWithTabStop ws.buffer ws.cursor.row ws.cursor.col ws.tabStop with
      | none => ws
      | some offset =>
          let b' := { ws.buffer with table := ws.buffer.table.insert offset "\n" offset, dirty := true }
          let b'' := FileBuffer.clearCache (FileBuffer.recomputeMissingEol b')
          { ws with buffer := b'', cursor := { row := ⟨ws.cursor.row.val + 1⟩, col := 0 } }
  | .backspace =>
      if ws.cursor.col.val > 0 then
        let prevC := ViE.prevCol ws.tabStop ws.buffer ws.cursor.row ws.cursor.col
        match ViE.getOffsetFromPointInBufferWithTabStop ws.buffer ws.cursor.row prevC ws.tabStop,
              ViE.getOffsetFromPointInBufferWithTabStop ws.buffer ws.cursor.row ws.cursor.col ws.tabStop with
        | some startOff, some endOff =>
            let len := endOff - startOff
            if len > 0 then
              let b' := { ws.buffer with table := ws.buffer.table.delete startOff len endOff, dirty := true }
              let b'' := FileBuffer.clearCache (FileBuffer.recomputeMissingEol b')
              { ws with buffer := b'', cursor := { ws.cursor with col := prevC } }
            else
              ws
        | _, _ => ws
      else if ws.cursor.row.val > 0 then
        let prevRow : Row := ⟨ws.cursor.row.val - 1⟩
        match ws.buffer.table.getLineRange prevRow.val with
        | some (start, len) =>
            let b' := { ws.buffer with table := ws.buffer.table.delete (start + len) 1 (start + len), dirty := true }
            let b'' := FileBuffer.clearCache (FileBuffer.recomputeMissingEol b')
            let newLen := ViE.lineDisplayWidth ws.tabStop b'' prevRow
            { ws with buffer := b'', cursor := { row := prevRow, col := ⟨newLen⟩ } }
        | none => ws
      else
        ws
private def applyWorkerStateToBuffer (s : EditorState) (bufferId : Nat) (ws : WorkerState) : EditorState :=
  let s1 := s.updateCurrentWorkspace fun cur =>
    { cur with
      buffers := cur.buffers.map fun b =>
        if b.id == bufferId then
          { ws.buffer with id := b.id, filename := b.filename, loaded := true, dirty := true }
        else
          b
    }
  let active := s1.getCurrentWorkspace.layout.findView s1.getCurrentWorkspace.activeWindowId
  let s2 :=
    match active with
    | some v =>
        if v.bufferId == bufferId then
          s1.setCursor ws.cursor
        else
          s1
    | none => s1
  { s2 with dirty := true }
private def enqueueInsertOp (s : EditorState) (op : InsertOp) : IO EditorState := do
  let ws := s.getCurrentWorkspace
  match ws.layout.findView ws.activeWindowId with
  | none => pure s
  | some view =>
      let bufferId := view.bufferId
      let key : WorkerKey := { sessionId := s.editSessionId, bufferId := bufferId }
      let snapshot : WorkerState := {
        buffer := s.getActiveBuffer
        cursor := view.cursor
        tabStop := s.config.tabStop
      }
      let sig := bufferSig snapshot.buffer
      let workers ← workersRef.get
      match workers.find? key with
      | none =>
          let t ← IO.asTask (pure (applyInsertOp snapshot op))
          let e : WorkerEntry := { baseSig := sig, submitted := 1, applied := 0, task := t }
          workersRef.set (workers.insert key e)
      | some e =>
          if e.baseSig == sig then
            let prev := e.task
            let t ← IO.asTask do
              match prev.get with
              | .ok st => pure (applyInsertOp st op)
              | .error err => throw err
            let e' : WorkerEntry := { e with submitted := e.submitted + 1, task := t }
            workersRef.set (workers.insert key e')
          else
            let t ← IO.asTask (pure (applyInsertOp snapshot op))
            let e' : WorkerEntry := { baseSig := sig, submitted := 1, applied := 0, task := t }
            workersRef.set (workers.insert key e')
      let s' :=
        match op with
        | .char c =>
            let delta := ViE.Unicode.charWidthAt s.config.tabStop view.cursor.col.val c
            s.setCursor { view.cursor with col := ⟨view.cursor.col.val + delta⟩ }
        | .newline =>
            s.setCursor { row := ⟨view.cursor.row.val + 1⟩, col := 0 }
        | .backspace =>
            if view.cursor.col.val > 0 then
              let prevC := ViE.prevCol s.config.tabStop s.getActiveBuffer view.cursor.row view.cursor.col
              s.setCursor { view.cursor with col := prevC }
            else if view.cursor.row.val > 0 then
              let prevRow : Row := ⟨view.cursor.row.val - 1⟩
              let newLen := ViE.lineDisplayWidth s.config.tabStop s.getActiveBuffer prevRow
              s.setCursor { row := prevRow, col := ⟨newLen⟩ }
            else
              s
      pure { s' with dirty := true }
def enqueueInsertChar (s : EditorState) (c : Char) : IO EditorState :=
  enqueueInsertOp s (.char c)
def enqueueInsertNewline (s : EditorState) : IO EditorState :=
  enqueueInsertOp s .newline
def enqueueBackspace (s : EditorState) : IO EditorState :=
  enqueueInsertOp s .backspace
def awaitActiveInsertOps (s : EditorState) : IO EditorState := do
  let ws := s.getCurrentWorkspace
  match ws.layout.findView ws.activeWindowId with
  | none => pure s
  | some view =>
      let bufferId := view.bufferId
      let key : WorkerKey := { sessionId := s.editSessionId, bufferId := bufferId }
      let workers ← workersRef.get
      match workers.find? key with
      | none => pure s
      | some e =>
          if e.applied >= e.submitted then
            workersRef.set (workers.erase key)
            pure s
          else
            let res := e.task.get
            workersRef.set (workers.erase key)
            match res with
            | .ok wsState => pure (applyWorkerStateToBuffer s bufferId wsState)
            | .error err => pure { s with message := s!"Insert worker error: {err}" }
def drainCompletedInsertOps (s : EditorState) : IO (EditorState × Bool) := do
  let workers ← workersRef.get
  let keys : Array WorkerKey := workers.fold (init := #[]) (fun acc k _ => acc.push k)
  let mut map := workers
  let mut st := s
  let mut changed := false
  for k in keys do
    match map.find? k with
    | none => pure ()
      | some e =>
          if e.applied >= e.submitted then
            map := map.erase k
          else
            let done ← IO.hasFinished e.task
            if done then
              let res := e.task.get
              map := map.erase k
              match res with
              | .ok wsState =>
                  if k.sessionId == s.editSessionId then
                    st := applyWorkerStateToBuffer st k.bufferId wsState
                  else
                    pure ()
                  changed := true
              | .error err =>
                  st := { st with message := s!"Insert worker error (session {k.sessionId}, buffer {k.bufferId}): {err}", dirty := true }
                  changed := true
  workersRef.set map
  pure (st, changed)
end ViE.Buffer.EditQueue

  let mut loadTasks : Array (Task (Except IO.Error FileBuffer)) := #[]
  for i in [0:filesArr.size] do
    let fname := filesArr[i]!
    if i == safeActiveIdx then
      let t ← IO.asTask (loadBufferByteArrayWithConfig fname settings)
      loadTasks := loadTasks.push t
    else
      -- Keep lazy placeholders semantically, but warm file cache in parallel.
      prefetchBufferByteArrayWithConfig fname settings
      let t ← IO.asTask (pure (emptyBuffer (some fname) buildLeafBits settings.searchBloomBuildOnEdit))
      loadTasks := loadTasks.push t

      let buf ← loadBufferByteArrayWithConfig fname settings

      let bufResult :=
        match loadTasks[i]? with
        | some t => t.get
        | none => Except.ok (emptyBuffer (some fname) buildLeafBits settings.searchBloomBuildOnEdit)
      let buf :=
        match bufResult with
        | Except.ok b => b
        | Except.error _ => emptyBuffer (some fname) buildLeafBits settings.searchBloomBuildOnEdit

    let prevState := state
    let (drainedState, drained) ← ViE.Buffer.EditQueue.drainCompletedInsertOps state
    state ←
      if drained then
        let synced ← ViE.Lsp.Lean.syncEditorUpdate prevState drainedState
        pure (ViE.enforceScroll synced)
      else
        pure drainedState

  let s_gbase ← runKeys s0 ([Key.char 'i'] ++ keys "line1\nline2\nline3" ++ [Key.esc])
  let s_gg_insert ← runKeys s_gbase [Key.char 'G', Key.char 'g', Key.char 'g', Key.char 'i', Key.char 'X', Key.esc]
  assertBuffer "insert after gg applies at moved cursor" s_gg_insert "Xline1\nline2\nline3"
  let s_G_insert ← runKeys s_gbase [Key.char 'g', Key.char 'g', Key.char 'G', Key.char 'i', Key.char 'Z', Key.esc]
  assertBuffer "insert after G applies at moved cursor" s_G_insert "line1\nline2\nZline3"