if h : lo < hi then

    if lo < hi then

      if h : lo < hi then

      if lo < hi then

/-- Find all occurrences of a byte pattern within a byte array. -/
partial def findAllMatchesBytes (haystack : ByteArray) (needle : ByteArray) : Array (Nat × Nat) :=
  let n := needle.size
  let h := haystack.size
  if n == 0 || h < n then
    #[]
  else
    let rec matchesAt (i j : Nat) : Bool :=
      if j == n then true
      else if haystack[i + j]! == needle[j]! then matchesAt i (j + 1) else false
    let rec loop (i : Nat) (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=
      if i + n > h then acc
      else
        let acc' := if matchesAt i 0 then acc.push (i, i + n) else acc
        loop (i + 1) acc'
    loop 0 #[]
def updateSearchLineCache (st : EditorState) (lineIdx : Row) (lineStr : String) (matchRanges : Array (Nat × Nat)) : EditorState :=
  match st.searchState with
  | none => st
  | some ss =>
      let lineMatches := ss.lineMatches.insert lineIdx (lineStr, matchRanges)
      let order :=
        if ss.lineOrder.contains lineIdx then
          ss.lineOrder
        else
          ss.lineOrder.push lineIdx
      let (lineMatches, order) :=
        if order.size > ss.lineCacheMax then
          let dropCount := order.size - ss.lineCacheMax
          let evicted := order.extract 0 dropCount
          let order := order.extract dropCount order.size
          let lineMatches := evicted.foldl (fun acc r => acc.erase r) lineMatches
          (lineMatches, order)
        else
          (lineMatches, order)
      { st with searchState := some { ss with lineMatches := lineMatches, lineOrder := order } }

      let prefetchSearchMatches (st : EditorState) (buf : FileBuffer) (startRow endRow : Nat) : EditorState :=
        match st.searchState with
        | none => st
        | some ss =>
            if ss.pattern.isEmpty then
              st
            else
              let totalLines := FileBuffer.lineCount buf
              let rec loop (row : Nat) (acc : EditorState) : EditorState :=
                if row >= endRow then
                  acc
                else if row >= totalLines then
                  acc
                else
                  let lineIdx : Row := ⟨row⟩
                  let lineStr := getLineFromBuffer buf lineIdx |>.getD ""
                  match acc.searchState with
                  | none => acc
                  | some ss2 =>
                      match ss2.lineMatches.find? lineIdx with
                      | some (cachedLine, _) =>
                          if cachedLine == lineStr then
                            loop (row + 1) acc
                          else
                            let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss2.pattern.toUTF8
                            let acc' := updateSearchLineCache acc lineIdx lineStr matchRanges
                            loop (row + 1) acc'
                      | none =>
                          let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss2.pattern.toUTF8
                          let acc' := updateSearchLineCache acc lineIdx lineStr matchRanges
                          loop (row + 1) acc'
              loop startRow st

      let prefetchMargin := 20
      let totalLines := FileBuffer.lineCount buf
      let startRow := if view.scrollRow.val > prefetchMargin then view.scrollRow.val - prefetchMargin else 0
      let endRow := min totalLines (view.scrollRow.val + workH + prefetchMargin)
      currentSt := prefetchSearchMatches currentSt buf startRow endRow

           let lineStr := cachedRaw.getD (getLineFromBuffer buf lineIdx |>.getD "")
           let lineIndex := cachedIdx.getD (ViE.Unicode.buildDisplayByteIndex lineStr)

                     | some raw, some idx =>

                     | some raw, some _ =>

                   | some raw, some idx =>

                   | some raw, some _ =>

           let (searchMatches, searchSt) :=
             match st.searchState with
             | some ss =>
                if ss.pattern.isEmpty then
                  (#[], currentSt)
                else
                  match ss.lineMatches.find? lineIdx with
                  | some (cachedLine, cachedMatches) =>
                      if cachedLine == lineStr then
                        (cachedMatches, currentSt)
                      else
                        let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss.pattern.toUTF8
                        let st' := updateSearchLineCache currentSt lineIdx lineStr matchRanges
                        (matchRanges, st')
                  | none =>
                      let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss.pattern.toUTF8
                      let st' := updateSearchLineCache currentSt lineIdx lineStr matchRanges
                      (matchRanges, st')
             | none => (#[], currentSt)
           currentSt := searchSt

           match selRange with
           | none => winBuf := winBuf.push displayLine
           | some _ =>

           let needsStyled := selRange.isSome || !searchMatches.isEmpty
           if !needsStyled then
             winBuf := winBuf.push displayLine
           else

             let cursorByte :=
               if lineIdx == view.cursor.row then
                 some (ViE.Unicode.displayColToByteOffsetFromIndex lineIndex view.cursor.col.val)
               else
                 none

                let byteStart := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex colVal
                let byteEnd := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex (colVal + w)

                let isMatched :=
                  searchMatches.any (fun (s, e) => byteStart < e && byteEnd > s)
                let isCursorMatch :=
                  match cursorByte with
                  | some cb => searchMatches.any (fun (s, e) => s <= cb && cb < e)
                  | none => false

                if isSelected && !styleActive then
                  winBuf := winBuf.push "\x1b[7m" -- Inverse video
                  styleActive := true
                else if !isSelected && styleActive then

                if isSelected then
                  if !styleActive then
                    winBuf := winBuf.push "\x1b[7m" -- Inverse video
                    styleActive := true
                else if isMatched then
                  if !styleActive then
                    if isCursorMatch then
                      winBuf := winBuf.push st.config.searchHighlightCursorStyle
                    else
                      winBuf := winBuf.push st.config.searchHighlightStyle
                    styleActive := true
                else if styleActive then

    else if state.mode == .searchForward then s!"/{state.inputState.commandBuffer}"
    else if state.mode == .searchBackward then s!"?{state.inputState.commandBuffer}"

     buffer := buffer.push (Terminal.moveCursorStr (rows - 1) (1 + state.inputState.commandBuffer.length))
  if state.mode == .searchForward || state.mode == .searchBackward then

  | searchForward
  | searchBackward

    | .searchForward => "SEARCH"
    | .searchBackward => "SEARCH"

  searchHighlightStyle : String
  searchHighlightCursorStyle : String
  searchBloomEnabled : Bool
  searchBloomMinBytes : Nat
  searchBloomCacheMax : Nat

  deriving Inhabited
inductive SearchDirection where
  | forward
  | backward
  deriving Repr, Inhabited, BEq
structure SearchState where
  pattern : String
  direction : SearchDirection
  useBloom : Bool
  lastMatch : Option Nat
  lastSearchOffset : Nat
  cache : Array Nat
  cacheMax : Nat
  lineMatches : Lean.RBMap Row (String × Array (Nat × Nat)) compare
  lineOrder : Array Row
  lineCacheMax : Nat
  bloomCache : Lean.RBMap Nat ByteArray compare
  bloomOrder : Array Nat
  bloomCacheMax : Nat
  deriving Inhabited
inductive RegisterKind where
  | charwise
  | linewise
  | blockwise
  deriving Repr, Inhabited, BEq
structure Register where
  kind : RegisterKind
  text : String
  blockLines : List String
  blockWidth : Nat

  lastSearchInputTime : Nat
  lastSearchRunTime : Nat
  pendingSearch : Bool

  clipboard : Option String -- Yank buffer (String instead of TextBuffer)

  clipboard : Option Register -- Yank buffer

  searchState : Option SearchState

import ViE.State.Search

  { s.exitVisualMode with clipboard := some text, message := s!"Yanked selection" }

  let reg : Register :=
    if s.mode == .visualBlock then
      let lines := if text.isEmpty then [] else text.splitOn "\n"
      let width := lines.foldl (fun m l => max m (ViE.Unicode.stringWidth l)) 0
      {
        kind := .blockwise
        text := text
        blockLines := lines
        blockWidth := width
      }
    else
      {
        kind := .charwise
        text := text
        blockLines := []
        blockWidth := 0
      }
  { s.exitVisualMode with clipboard := some reg, message := s!"Yanked selection" }

      let text := s.getSelectedText
      let lines := if text.isEmpty then [] else text.splitOn "\n"
      let width := lines.foldl (fun m l => max m (ViE.Unicode.stringWidth l)) 0
      let reg : Register := {
        kind := .blockwise
        text := text
        blockLines := lines
        blockWidth := width
      }

      s'.exitVisualMode |>.setCursor { row := ⟨minRow⟩, col := ⟨minCol⟩ }

      { s'.exitVisualMode with clipboard := some reg } |>.setCursor { row := ⟨minRow⟩, col := ⟨minCol⟩ }

      let text := s.getSelectedText
      let reg : Register := {
        kind := .charwise
        text := text
        blockLines := []
        blockWidth := 0
      }

      s'.exitVisualMode |>.setCursor p1

      { s'.exitVisualMode with clipboard := some reg } |>.setCursor p1

import ViE.State.Layout
import ViE.State.Movement
import ViE.Types
import ViE.Buffer.Content
import ViE.Data.PieceTable
import ViE.Data.PieceTable.Tree
namespace ViE
def searchChunkSize : Nat := 8192
def incrementalSearchDebounceMs : Nat := 120
def updateSearchCache (state : SearchState) (offset : Nat) : SearchState :=
  let cache := state.cache.push offset
  let cache :=
    if cache.size > state.cacheMax then
      cache.extract (cache.size - state.cacheMax) cache.size
    else
      cache
  { state with cache := cache }
def getCursorOffset (s : EditorState) : Nat :=
  let buf := s.getActiveBuffer
  let cursor := s.getCursor
  ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0
def applyMatchOffset (s : EditorState) (offset : Nat) : EditorState :=
  let buf := s.getActiveBuffer
  let (r, c) := buf.table.getPointFromOffset offset
  s.setCursor { row := ⟨r⟩, col := ⟨c⟩ }
def startSearch (s : EditorState) (pattern : String) (direction : SearchDirection) (useBloom : Bool) : EditorState :=
  let cursorOffset := getCursorOffset s
  let search : SearchState := {
    pattern := pattern
    direction := direction
    useBloom := useBloom
    lastMatch := none
    lastSearchOffset := cursorOffset
    cache := #[]
    cacheMax := 128
    lineMatches := Lean.RBMap.empty
    lineOrder := #[]
    lineCacheMax := 512
    bloomCache := Lean.RBMap.empty
    bloomOrder := #[]
    bloomCacheMax := s.config.searchBloomCacheMax
  }
  { s with searchState := some search }
def startOrUpdateSearch (s : EditorState) (pattern : String) (direction : SearchDirection) (useBloom : Bool) : EditorState :=
  match s.searchState with
  | none => startSearch s pattern direction useBloom
  | some st =>
      let cursorOffset := getCursorOffset s
      let st' := {
        st with
          pattern := pattern
          direction := direction
          useBloom := useBloom
          lastMatch := none
          lastSearchOffset := cursorOffset
          cache := #[]
          lineMatches := Lean.RBMap.empty
          lineOrder := #[]
      }
      { s with searchState := some st' }
def searchNextOffset (pt : PieceTable) (pattern : ByteArray) (startOffset : Nat) (useBloom : Bool)
  (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat)
  : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
  PieceTree.searchNext pt.tree pt pattern startOffset searchChunkSize useBloom cache order cacheMax
def searchPrevOffset (pt : PieceTable) (pattern : ByteArray) (startExclusive : Nat) (useBloom : Bool)
  (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat)
  : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
  PieceTree.searchPrev pt.tree pt pattern startExclusive searchChunkSize useBloom cache order cacheMax
def findNextMatch (s : EditorState) (directionOverride : Option SearchDirection := none) : EditorState :=
  match s.searchState with
  | none => { s with message := "No search pattern" }
  | some st =>
    let direction := directionOverride.getD st.direction
    if st.pattern.isEmpty then
      { s with message := "Empty search pattern" }
    else
      let pt := s.getActiveBuffer.table
      let patBytes := st.pattern.toUTF8
      let startOffset :=
        match direction with
        | .forward =>
          match st.lastMatch with
          | some m => m + 1
          | none => getCursorOffset s
        | .backward =>
          match st.lastMatch with
          | some m => m
          | none => getCursorOffset s
      let useBloom := st.useBloom && patBytes.size >= 3
      let (result, bloomCache, bloomOrder) :=
        match direction with
        | .forward => searchNextOffset pt patBytes startOffset useBloom st.bloomCache st.bloomOrder st.bloomCacheMax
        | .backward => searchPrevOffset pt patBytes startOffset useBloom st.bloomCache st.bloomOrder st.bloomCacheMax
      let (result, wrapped, bloomCache, bloomOrder) :=
        match result, direction with
        | some r, _ => (some r, false, bloomCache, bloomOrder)
        | none, .forward =>
            if startOffset > 0 then
              let (r2, c2, o2) := searchNextOffset pt patBytes 0 useBloom bloomCache bloomOrder st.bloomCacheMax
              (r2, true, c2, o2)
            else
              (none, false, bloomCache, bloomOrder)
        | none, .backward =>
            let total := pt.tree.length
            if startOffset < total then
              let (r2, c2, o2) := searchPrevOffset pt patBytes total useBloom bloomCache bloomOrder st.bloomCacheMax
              (r2, true, c2, o2)
            else
              (none, false, bloomCache, bloomOrder)
      match result with
      | none =>
          let st' := { st with bloomCache := bloomCache, bloomOrder := bloomOrder }
          { s with searchState := some st', message := s!"Pattern not found: {st.pattern}" }
      | some off =>
          let s' := applyMatchOffset s off
          let st' := updateSearchCache { st with lastMatch := some off, bloomCache := bloomCache, bloomOrder := bloomOrder } off
          let st'' := { st' with direction := direction }
          let bloomTag := if useBloom then " [bloom]" else ""
          let msg :=
            if wrapped then
              s!"Wrapped: {st.pattern}{bloomTag}"
            else
              s!"Match: {st.pattern}{bloomTag}"
          { s' with searchState := some st'', message := msg }
def runIncrementalSearch (s : EditorState) : EditorState :=
  if s.mode != .searchForward && s.mode != .searchBackward then
    s
  else
    let pattern := s.inputState.commandBuffer
    if pattern.isEmpty then
      s
    else
      let direction := if s.mode == .searchBackward then SearchDirection.backward else SearchDirection.forward
      let s' := startOrUpdateSearch s pattern direction false
      findNextMatch s' (some direction)
def maybeRunIncrementalSearch (s : EditorState) (now : Nat) : EditorState :=
  if s.inputState.pendingSearch && now - s.inputState.lastSearchInputTime >= incrementalSearchDebounceMs then
    let s' := runIncrementalSearch s
    { s' with
      dirty := true
      inputState := { s'.inputState with pendingSearch := false, lastSearchRunTime := now }
    }
  else
    s
end ViE

    if h : wg.currentWorkspace < wg.workspaces.size then

    if wg.currentWorkspace < wg.workspaces.size then

  let deletedText :=
    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,
          ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with
    | some startOff, some endOff =>
        if cursor.col.val < lineLen && endOff > startOff then
          PieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.table
        else
          ""
    | _, _ => ""

  let newBuffer := s'.getActiveBuffer

  let s'' :=
    if deletedText.isEmpty then
      s'
    else
      let reg : Register := {
        kind := .charwise
        text := deletedText
        blockLines := []
        blockWidth := 0
      }
      { s' with clipboard := some reg }
  let newBuffer := s''.getActiveBuffer

     s'.setCursor { cursor with col := ⟨newCol⟩ }

     s''.setCursor { cursor with col := ⟨newCol⟩ }

     s'

     s''

  let line := ViE.getLineFromBuffer s.getActiveBuffer cursor.row |>.getD ""
  let content := if line.endsWith "\n" then line else line ++ "\n"
  let reg : Register := {
    kind := .linewise
    text := content
    blockLines := []
    blockWidth := 0
  }

    clipboard := some reg,

  let buffer := s.getActiveBuffer
  let (startOffOpt, endOffOpt) :=
    match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,
          ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with
    | some off1, some off2 => (some (min off1 off2), some (max off1 off2))
    | _, _ => (none, none)
  let deletedText :=
    match (startOffOpt, endOffOpt) with
    | (some startOff, some endOff) =>
        if endOff > startOff then
          PieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.table
        else
          ""
    | _ => ""

     match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,
           ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with
     | some off1, some off2 =>
         let startOff := min off1 off2
         let endOff := max off1 off2

     match (startOffOpt, endOffOpt) with
     | (some startOff, some endOff) =>

     | _, _ => buffer

     | _ => buffer

  { s'' with inputState := { s''.inputState with previousKey := none } }

  let s''' :=
    if deletedText.isEmpty then
      s''
    else
      let reg : Register := {
        kind := .charwise
        text := deletedText
        blockLines := []
        blockWidth := 0
      }
      { s'' with clipboard := some reg }
  { s''' with inputState := { s'''.inputState with previousKey := none } }

  { s with clipboard := (some content : Option String), message := "Yanked 1 line" }

  let reg : Register := {
    kind := .linewise
    text := content
    blockLines := []
    blockWidth := 0
  }
  { s with clipboard := some reg, message := "Yanked 1 line" }
def EditorState.ensureLineCount (s : EditorState) (count : Nat) : EditorState :=
  s.updateActiveBuffer fun buffer =>
    let lineCount := buffer.table.lineCount
    if count <= lineCount then
      buffer
    else
      let missing := count - lineCount
      let newlines := String.ofList (List.replicate missing '\n')
      let len := buffer.table.tree.length
      { buffer with table := buffer.table.insert len newlines len, dirty := true }
def EditorState.pasteCharwise (s : EditorState) (text : String) (after : Bool) : EditorState :=
  let cursor := s.getCursor
  let line := ViE.getLineFromBuffer s.getActiveBuffer cursor.row |>.getD ""
  let lineWidth := ViE.Unicode.stringWidth line
  let targetCol :=
    if after then
      if cursor.col.val < lineWidth then
        ViE.Unicode.nextDisplayCol line cursor.col.val
      else
        cursor.col.val
    else
      cursor.col.val
  let s' := s.updateActiveBuffer fun buffer =>
    match ViE.getOffsetFromPointInBuffer buffer cursor.row.val targetCol with
    | some offset => { buffer with table := buffer.table.insert offset text offset, dirty := true }
    | none => buffer
  let lines := text.splitOn "\n"
  let lastLine := lines.getLastD ""
  let lastWidth := ViE.Unicode.stringWidth lastLine
  let rowDelta := if lines.length > 0 then lines.length - 1 else 0
  let newRow := cursor.row.val + rowDelta
  let newCol :=
    if lines.length <= 1 then
      if lastWidth == 0 then targetCol else targetCol + lastWidth - 1
    else
      if lastWidth == 0 then 0 else lastWidth - 1
  s'.setCursor { row := ⟨newRow⟩, col := ⟨newCol⟩ }
def firstNonBlankCol (line : String) : Nat :=
  let rec loop (cs : List Char) (col : Nat) : Nat :=
    match cs with
    | [] => 0
    | c :: rest =>
      if c == ' ' || c == '\t' then
        loop rest (col + ViE.Unicode.charWidth c)
      else
        col
  loop line.toList 0
def EditorState.pasteLinewise (s : EditorState) (text : String) (below : Bool) : EditorState :=
  let cursor := s.getCursor
  let row := if below then cursor.row.val + 1 else cursor.row.val
  let s' := s.updateActiveBuffer fun buffer =>
    -- Determine insert offset.
    -- Try start of target line. If EOF, append.
    let (offset, textToInsert) := match ViE.getOffsetFromPointInBuffer buffer row 0 with
                  | some off => (off, text)
                  | none =>
                      let len := buffer.table.tree.length
                      if len > 0 then
                         if !PieceTable.endsWithNewline buffer.table then
                             (len, "\n" ++ text)
                         else
                             (len, text)
                      else (0, text)
    let pt := buffer.table.commit
    { buffer with table := pt.insert offset textToInsert offset, dirty := true }
  let newRow := if below then cursor.row.val + 1 else cursor.row.val
  let lineStr := ViE.getLineFromBuffer s'.getActiveBuffer ⟨newRow⟩ |>.getD ""
  let col := firstNonBlankCol lineStr
  s'.setCursor { row := ⟨newRow⟩, col := ⟨col⟩ }
def EditorState.pasteBlockwise (s : EditorState) (reg : Register) (after : Bool) : EditorState :=
  let cursor := s.getCursor
  let line := ViE.getLineFromBuffer s.getActiveBuffer cursor.row |>.getD ""
  let lineWidth := ViE.Unicode.stringWidth line
  let baseCol :=
    if after then
      if cursor.col.val < lineWidth then
        ViE.Unicode.nextDisplayCol line cursor.col.val
      else
        cursor.col.val
    else
      cursor.col.val
  let lines :=
    if reg.blockLines.isEmpty then
      if reg.text.isEmpty then [] else reg.text.splitOn "\n"
    else
      reg.blockLines
  let targetLineCount := cursor.row.val + lines.length
  let s1 := s.ensureLineCount targetLineCount
  let s2 := s1.updateActiveBuffer fun buffer =>
    let rec apply (buf : FileBuffer) (idx : Nat) (ls : List String) : FileBuffer :=
      match ls with
      | [] => buf
      | l :: rest =>
        let row := cursor.row.val + idx
        let lineStr := ViE.getLineFromBuffer buf ⟨row⟩ |>.getD ""
        let lineW := ViE.Unicode.stringWidth lineStr
        let targetCol := baseCol
        let (buf1, offset) :=
          if targetCol > lineW then
            let pad := targetCol - lineW
            let padStr := String.ofList (List.replicate pad ' ')
            let insertOff := ViE.getOffsetFromPointInBuffer buf row lineW |>.getD (buf.table.tree.length)
            let buf' := { buf with table := buf.table.insert insertOff padStr insertOff, dirty := true }
            let off' := ViE.getOffsetFromPointInBuffer buf' row targetCol |>.getD insertOff
            (buf', off')
          else
            let off := ViE.getOffsetFromPointInBuffer buf row targetCol |>.getD 0
            (buf, off)
        let buf2 := { buf1 with table := buf1.table.insert offset l offset, dirty := true }
        apply buf2 (idx + 1) rest
    apply buffer 0 lines
  s2.setCursor { row := cursor.row, col := ⟨baseCol⟩ }

  | some text =>
    let cursor := s.getCursor
    let s' := s.updateActiveBuffer fun buffer =>
      -- Determine insert offset.
      -- Try start of next line. If EOF, append.
      let (offset, textToInsert) := match ViE.getOffsetFromPointInBuffer buffer (cursor.row.val + 1) 0 with
                    | some off => (off, text)
                    | none =>
                        let len := buffer.table.tree.length
                        if len > 0 then
                           -- Check if buffer ends with newline to avoid merging
                           -- (Optimization: ideally check last char directly)
                           if !PieceTable.endsWithNewline buffer.table then
                               (len, "\n" ++ text)
                           else
                               (len, text)
                        else (0, text)

  | some reg =>
    match reg.kind with
    | .linewise => s.pasteLinewise reg.text true
    | .charwise => s.pasteCharwise reg.text true
    | .blockwise => s.pasteBlockwise reg true

      -- For paste, undo should restore cursor to insertion point
      let pt := buffer.table.commit
      { buffer with table := pt.insert offset textToInsert offset
                    dirty := true }
    s'.setCursor { row := ⟨cursor.row.val + 1⟩, col := 0 }

  | some text =>
    let cursor := s.getCursor
    let s' := s.updateActiveBuffer fun buffer =>
      let offset := match ViE.getOffsetFromPointInBuffer buffer cursor.row.val 0 with
                     | some off => off
                     | none => 0
       let pt := buffer.table.commit
       let textStr : String := text
       { buffer with table := pt.insert offset textStr offset
                     dirty := true }
    s'.setCursor { cursor with col := 0 }

  | some reg =>
    match reg.kind with
    | .linewise => s.pasteLinewise reg.text false
    | .charwise => s.pasteCharwise reg.text false
    | .blockwise => s.pasteBlockwise reg false

  searchHighlightStyle := (ViE.Color.toBg .white) ++ (ViE.Color.toFg .black)
  searchHighlightCursorStyle := (ViE.Color.toBg .yellow) ++ (ViE.Color.toFg .black)
  searchBloomEnabled := false
  searchBloomMinBytes := 64 * 1024 * 1024
  searchBloomCacheMax := 1024

  lastSearchInputTime := 0
  lastSearchRunTime := 0
  pendingSearch := false

  searchState := none

  | Key.char '/' =>
      pure {
        s with
          mode := Mode.searchForward
          inputState := {
            s.inputState with
              commandBuffer := ""
              countBuffer := ""
              previousKey := none
              pendingSearch := false
          }
      }
  | Key.char '?' =>
      pure {
        s with
          mode := Mode.searchBackward
          inputState := {
            s.inputState with
              commandBuffer := ""
              countBuffer := ""
              previousKey := none
              pendingSearch := false
          }
      }

  | Key.char 'n' => pure $ clearInput (ViE.findNextMatch s)
  | Key.char 'N' =>
      let overrideDir :=
        match s.searchState with
        | some st =>
            if st.direction == .forward then some SearchDirection.backward else some SearchDirection.forward
        | none => none
      pure $ clearInput (ViE.findNextMatch s overrideDir)

  | _ => return state
def handleSearchInput (state : EditorState) (k : Key) : IO EditorState := do
  match k with
  | Key.esc =>
      return {
        state with
          mode := .normal
          inputState := { state.inputState with commandBuffer := "", pendingSearch := false }
      }
  | Key.enter =>
      let pattern := state.inputState.commandBuffer
      if pattern.isEmpty then
        return {
          state with
            mode := .normal
            message := "Empty search pattern"
            inputState := { state.inputState with commandBuffer := "", pendingSearch := false }
        }
      else
        let direction := if state.mode == .searchBackward then SearchDirection.backward else SearchDirection.forward
        let s' :=
          match state.searchState with
          | some st =>
              if st.pattern == pattern && st.direction == direction then
                state
              else
                ViE.startOrUpdateSearch state pattern direction false
          | none =>
              ViE.startOrUpdateSearch state pattern direction false
        let s'' := ViE.findNextMatch s' (some direction)
        return {
          s'' with
            mode := .normal
            inputState := { s''.inputState with commandBuffer := "", pendingSearch := false }
        }
  | Key.backspace =>
      if state.inputState.commandBuffer.length > 0 then
        let newCmd := state.inputState.commandBuffer.dropEnd 1
        let now ← IO.monoMsNow
        let s1 := {
          state with
            inputState := {
              state.inputState with
                commandBuffer := newCmd.toString
                lastSearchInputTime := now
                pendingSearch := true
            }
        }
        if now - state.inputState.lastSearchRunTime >= ViE.incrementalSearchDebounceMs then
          let s2 := ViE.runIncrementalSearch s1
          return { s2 with inputState := { s2.inputState with pendingSearch := false, lastSearchRunTime := now } }
        else
          return s1
      else
        return state
  | Key.char c =>
      let now ← IO.monoMsNow
      let s1 := {
        state with
          inputState := {
            state.inputState with
              commandBuffer := state.inputState.commandBuffer.push c
              lastSearchInputTime := now
              pendingSearch := true
          }
      }
      if now - state.inputState.lastSearchRunTime >= ViE.incrementalSearchDebounceMs then
        let s2 := ViE.runIncrementalSearch s1
        return { s2 with inputState := { s2.inputState with pendingSearch := false, lastSearchRunTime := now } }
      else
        return s1

  | .searchForward => ViE.Key.handleSearchInput state k
  | .searchBackward => ViE.Key.handleSearchInput state k

    let tree := PieceTree.fromPieces pieces

    let tmpPt : PieceTable := { original := bytes, addBuffers := #[], tree := PieceTree.empty, undoStack := [], redoStack := [], undoStackCount := 0, redoStackCount := 0, undoLimit := 100, lastInsert := none }
    let tree := PieceTree.fromPieces pieces tmpPt

    let mid := PieceTree.fromPieces newPieces
    let newTree := PieceTree.concat (PieceTree.concat l mid) r

    let mid := PieceTree.fromPieces newPieces pt'
    let newTree := PieceTree.concat (PieceTree.concat l mid pt') r pt'

    }
/-- Insert text without touching undo/redo stacks (internal for bulk edits). -/
def PieceTable.insertRaw (pt : PieceTable) (offset : Nat) (text : String) : PieceTable :=
  if text.isEmpty then pt
  else
    let (pt', newPieces) := PieceTableHelper.appendText pt text
    let (l, r) := PieceTree.split pt.tree offset pt'
    let mid := PieceTree.fromPieces newPieces pt'
    let newTree := PieceTree.concat (PieceTree.concat l mid pt') r pt'
    { pt' with tree := newTree, lastInsert := none }
/-- Delete a range without touching undo/redo stacks (internal for bulk edits). -/
def PieceTable.deleteRaw (pt : PieceTable) (offset : Nat) (length : Nat) : PieceTable :=
  if length == 0 then pt
  else
    let newTree := PieceTree.delete pt.tree offset length pt
    { pt with tree := newTree, lastInsert := none }
/-- Apply a list of replacements as a single undoable edit. -/
def PieceTable.applyReplacements (pt : PieceTable) (cursorOffset : Nat) (replacements : Array (Nat × Nat)) (newText : String) : PieceTable :=
  if replacements.isEmpty then
    pt
  else
    let oldTree := pt.tree
    let pt' := Id.run do
      let mut acc := pt
      for (startOff, endOff) in replacements.reverse do
        let len := endOff - startOff
        acc := acc.deleteRaw startOff len
        acc := acc.insertRaw startOff newText
      return acc
    let stack := (oldTree, cursorOffset) :: pt'.undoStack
    let newCount := pt'.undoStackCount + 1
    let (finalStack, finalCount) :=
      if newCount > pt'.undoLimit then
        (stack.take pt'.undoLimit, pt'.undoLimit)
      else
        (stack, newCount)
    { pt' with
      undoStack := finalStack
      undoStackCount := finalCount
      redoStack := []
      redoStackCount := 0
      lastInsert := none

/-- Apply deletions as a single undoable edit. -/
def PieceTable.applyDeletions (pt : PieceTable) (cursorOffset : Nat) (ranges : Array (Nat × Nat)) : PieceTable :=
  PieceTable.applyReplacements pt cursorOffset ranges ""

import Lean

  | ViE.PieceTree.leaf _ s => s
  | ViE.PieceTree.internal _ s => s

  | ViE.PieceTree.leaf _ s _ => s
  | ViE.PieceTree.internal _ s _ => s

def searchMetaOf (t : ViE.PieceTree) : ViE.SearchBloom :=
  match t with
  | ViE.PieceTree.empty => ViE.SearchBloom.empty
  | ViE.PieceTree.leaf _ _ m => m
  | ViE.PieceTree.internal _ _ m => m
def bloomOr (a b : ByteArray) : ByteArray := Id.run do
  let mut out := a
  let size := min a.size b.size
  for i in [0:size] do
    out := out.set! i (out[i]! ||| b[i]!)
  out
def bloomSetBit (bloom : ByteArray) (idx : Nat) : ByteArray :=
  let byteIdx := idx / 8
  let bitIdx := idx % 8
  if byteIdx < bloom.size then
    let cur := bloom[byteIdx]!
    let mask : UInt8 := UInt8.ofNat (1 <<< bitIdx)
    bloom.set! byteIdx (cur ||| mask)
  else
    bloom
def bloomGetBit (bloom : ByteArray) (idx : Nat) : Bool :=
  let byteIdx := idx / 8
  let bitIdx := idx % 8
  if byteIdx < bloom.size then
    let cur := bloom[byteIdx]!
    let mask : UInt8 := UInt8.ofNat (1 <<< bitIdx)
    (cur &&& mask) != 0
  else
    false
def hash1 (b0 b1 b2 : UInt8) : Nat :=
  (b0.toNat * 961 + b1.toNat * 31 + b2.toNat) % ViE.BloomBits
def hash2 (b0 b1 b2 : UInt8) : Nat :=
  (b0.toNat * 17161 + b1.toNat * 131 + b2.toNat) % ViE.BloomBits
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 addTrigramsFromArray (bloom : ByteArray) (arr : Array UInt8) : ByteArray := Id.run do
  if arr.size < 3 then
    return bloom
  let limit := arr.size - 2
  let mut out := bloom
  for i in [0:limit] do
    out := addTrigramToBloom out arr[i]! arr[i + 1]! arr[i + 2]!
  return out
def takeFirstBytes (arr : Array UInt8) (n : Nat) : Array UInt8 :=
  if arr.size <= n then arr else arr.extract 0 n
def takeLastBytes (arr : Array UInt8) (n : Nat) : Array UInt8 :=
  if arr.size <= n then arr else arr.extract (arr.size - n) arr.size
partial def buildPrefixBytes (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : Array UInt8 :=
  let rec loop (i : Nat) (acc : Array UInt8) : Array UInt8 :=
    if i >= pieces.size || acc.size >= 2 then
      acc
    else
      let p := pieces[i]!
      let buf := PieceTableHelper.getBuffer pt p.source
      let slice := buf.extract p.start (p.start + p.length)
      if slice.size > 0 then
        let need := 2 - acc.size
        let take := takeFirstBytes slice.data need
        loop (i + 1) (acc ++ take)
      else
        loop (i + 1) acc
  loop 0 #[]
partial def buildSuffixBytes (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : Array UInt8 :=
  let rec loop (i : Nat) (acc : Array UInt8) : Array UInt8 :=
    if i == 0 || acc.size >= 2 then
      acc
    else
      let idx := i - 1
      let p := pieces[idx]!
      let buf := PieceTableHelper.getBuffer pt p.source
      let slice := buf.extract p.start (p.start + p.length)
      if slice.size > 0 then
        let need := 2 - acc.size
        let take := takeLastBytes slice.data need
        loop idx (take ++ acc)
      else
        loop idx acc
  loop pieces.size #[]
def addBytesToBloom (bloom : ByteArray) (carry : Array UInt8) (bytes : ByteArray) : (ByteArray × Array UInt8) :=
  let arr := carry ++ bytes.data
  let bloom' := addTrigramsFromArray bloom arr
  let carry' := takeLastBytes arr 2
  (bloom', carry')
def addBoundaryTrigrams (bloom : ByteArray) (leftSuffix rightPrefix : Array UInt8) : ByteArray :=
  let combined := leftSuffix ++ rightPrefix
  addTrigramsFromArray bloom combined
def buildBloomForPieces (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : ViE.SearchBloom := Id.run do
  if !ViE.BloomBuildLeafBits then
    let prefixBytes := buildPrefixBytes pieces pt
    let suffixBytes := buildSuffixBytes pieces pt
    return { bits := ViE.SearchBloom.empty.bits, prefixBytes := prefixBytes, suffixBytes := suffixBytes }
  else
    let mut bits := ViE.SearchBloom.empty.bits
    let mut carry : Array UInt8 := #[]
    let mut prefixBytes : Array UInt8 := #[]
    for p in pieces do
      let buf := PieceTableHelper.getBuffer pt p.source
      let slice := buf.extract p.start (p.start + p.length)
      if prefixBytes.size < 2 && slice.size > 0 then
        let need := 2 - prefixBytes.size
        let arr := slice.data
        let take := takeFirstBytes arr need
        prefixBytes := prefixBytes ++ take
      let (bits', carry') := addBytesToBloom bits carry slice
      bits := bits'
      carry := carry'
    return { bits := bits, prefixBytes := prefixBytes, suffixBytes := carry }

def bloomIsEmpty (bloom : ByteArray) : Bool :=
  bloom.data.all (fun b => b == 0)
def combineBloom (left right : ViE.SearchBloom) : ViE.SearchBloom :=
  let pref :=
    if left.prefixBytes.size >= 2 then left.prefixBytes
    else takeFirstBytes (left.prefixBytes ++ right.prefixBytes) 2
  let suf :=
    if right.suffixBytes.size >= 2 then right.suffixBytes
    else takeLastBytes (left.suffixBytes ++ right.suffixBytes) 2
  -- If any child bloom is empty (unknown), keep bits empty to avoid false negatives.
  if bloomIsEmpty left.bits || bloomIsEmpty right.bits then
    { bits := ViE.SearchBloom.empty.bits, prefixBytes := pref, suffixBytes := suf }
  else
    let bits := bloomOr left.bits right.bits
    let bits := addBoundaryTrigrams bits left.suffixBytes right.prefixBytes
    { bits := bits, prefixBytes := pref, suffixBytes := suf }
def buildBloomForChildren (children : Array ViE.PieceTree) : ViE.SearchBloom := Id.run do
  if children.isEmpty then
    return ViE.SearchBloom.empty
  let mut acc := searchMetaOf children[0]!
  for i in [1:children.size] do
    acc := combineBloom acc (searchMetaOf children[i]!)
  return acc
def patternTrigramHashes (pattern : ByteArray) : Array (Nat × Nat) := Id.run do
  if pattern.size < 3 then
    return #[]
  let arr := pattern.data
  let limit := pattern.size - 2
  let mut hashes : Array (Nat × Nat) := #[]
  for i in [0:limit] do
    let b0 := arr[i]!
    let b1 := arr[i + 1]!
    let b2 := arr[i + 2]!
    hashes := hashes.push (hash1 b0 b1 b2, hash2 b0 b1 b2)
  return hashes
def bloomMayContain (bloom : ByteArray) (hashes : Array (Nat × Nat)) : Bool :=
  if hashes.isEmpty then
    true
  else if bloomIsEmpty bloom then
    -- Empty bloom means "unknown", do not prune.
    true
  else
    hashes.all (fun (h1, h2) => bloomGetBit bloom h1 && bloomGetBit bloom h2)
def cacheInsert (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (maxSize : Nat) (key : Nat) (value : ByteArray)
  : (Lean.RBMap Nat ByteArray compare × Array Nat) :=
  let cache := cache.insert key value
  let order := if order.contains key then order else order.push key
  if order.size > maxSize then
    let dropCount := order.size - maxSize
    let evicted := order.extract 0 dropCount
    let order := order.extract dropCount order.size
    let cache := evicted.foldl (fun acc k => acc.erase k) cache
    (cache, order)
  else
    (cache, order)
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')

def mkLeaf (pieces : Array ViE.Piece) : ViE.PieceTree :=

def mkLeaf (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : ViE.PieceTree :=

  ViE.PieceTree.leaf pieces s

  let searchMeta := buildBloomForPieces pieces pt
  ViE.PieceTree.leaf pieces s searchMeta

  ViE.PieceTree.internal children s

  let searchMeta := buildBloomForChildren children
  ViE.PieceTree.internal children s searchMeta

partial def fromPieces (pieces : Array ViE.Piece) : ViE.PieceTree :=

partial def fromPieces (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : ViE.PieceTree :=

    mkLeaf pieces

    mkLeaf pieces pt

    let left := fromPieces (pieces.extract 0 mid)
    let right := fromPieces (pieces.extract mid pieces.size)

    let left := fromPieces (pieces.extract 0 mid) pt
    let right := fromPieces (pieces.extract mid pieces.size) pt

partial def concat (l : ViE.PieceTree) (r : ViE.PieceTree) : ViE.PieceTree :=

partial def concat (l : ViE.PieceTree) (r : ViE.PieceTree) (pt : ViE.PieceTable) : ViE.PieceTree :=

  | ViE.PieceTree.leaf ps1 _, ViE.PieceTree.leaf ps2 _ =>

  | ViE.PieceTree.leaf ps1 _ _, ViE.PieceTree.leaf ps2 _ _ =>

          mkLeaf ps

          mkLeaf ps pt

          mkInternal #[mkLeaf (ps.extract 0 mid), mkLeaf (ps.extract mid ps.size)]

          mkInternal #[mkLeaf (ps.extract 0 mid) pt, mkLeaf (ps.extract mid ps.size) pt]

        if ps.size <= ViE.NodeCapacity then mkLeaf ps
        else mkInternal #[mkLeaf ps1, mkLeaf ps2]

        if ps.size <= ViE.NodeCapacity then mkLeaf ps pt
        else mkInternal #[mkLeaf ps1 pt, mkLeaf ps2 pt]

  | ViE.PieceTree.internal cs1 _, ViE.PieceTree.internal cs2 _ =>

  | ViE.PieceTree.internal cs1 _ _, ViE.PieceTree.internal cs2 _ _ =>

      let merged := concat lastChild firstChild

      let merged := concat lastChild firstChild pt

      | ViE.PieceTree.internal newCS s =>

      | ViE.PieceTree.internal newCS s _ =>

      let newLast := concat lastChild r

      let newLast := concat lastChild r pt

      | ViE.PieceTree.internal newChildren s =>

      | ViE.PieceTree.internal newChildren s _ =>

      let newFirst := concat l firstChild

      let newFirst := concat l firstChild pt

      | ViE.PieceTree.internal newChildren s =>

      | ViE.PieceTree.internal newChildren s _ =>

  | ViE.PieceTree.leaf .. , ViE.PieceTree.internal .. => concat (mkInternal #[l]) r
  | ViE.PieceTree.internal .. , ViE.PieceTree.leaf .. => concat l (mkInternal #[r])

  | ViE.PieceTree.leaf .. , ViE.PieceTree.internal .. => concat (mkInternal #[l]) r pt
  | ViE.PieceTree.internal .. , ViE.PieceTree.leaf .. => concat l (mkInternal #[r]) pt

  | ViE.PieceTree.leaf pieces _ =>

  | ViE.PieceTree.leaf pieces _ _ =>

             (mkLeaf (pieces.extract 0 i), mkLeaf (pieces.extract i pieces.size))

             (mkLeaf (pieces.extract 0 i) pt, mkLeaf (pieces.extract i pieces.size) pt)

             (mkLeaf ((pieces.extract 0 i).push p1), mkLeaf (#[p2] ++ (pieces.extract (i + 1) pieces.size)))

             (mkLeaf ((pieces.extract 0 i).push p1) pt, mkLeaf (#[p2] ++ (pieces.extract (i + 1) pieces.size)) pt)

  | ViE.PieceTree.internal children _ =>

  | ViE.PieceTree.internal children _ _ =>

  concat l r

  concat l r pt

/-- Get substring from tree -/
partial def getSubstring (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : String :=

/-- Get bytes from tree -/
partial def getBytes (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : ByteArray :=

      | ViE.PieceTree.leaf pieces _ =>

      | ViE.PieceTree.leaf pieces _ _ =>

      | ViE.PieceTree.internal children _ =>

      | ViE.PieceTree.internal children _ _ =>

  let combined := chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])
  String.fromUTF8! combined

  chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])
/-- Get substring from tree -/
partial def getSubstring (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : String :=
  String.fromUTF8! (getBytes t offset len pt)

    | ViE.PieceTree.leaf pieces _ =>

    | ViE.PieceTree.leaf pieces _ _ =>

    | ViE.PieceTree.internal children _ =>

    | ViE.PieceTree.internal children _ _ =>

partial def maximalSuffixLoop (x : ByteArray) (useLe : Bool) (m ms j k p : Int) : (Int × Int) :=
  if j + k >= m then
    (ms, p)
  else
    let a := x[Int.toNat (j + k)]!
    let b := x[Int.toNat (ms + k)]!
    if useLe then
      if a < b then
        maximalSuffixLoop x useLe m ms (j + k) 1 (j + k - ms)
      else if a == b then
        if k != p then
          maximalSuffixLoop x useLe m ms j (k + 1) p
        else
          maximalSuffixLoop x useLe m ms (j + p) 1 p
      else
        maximalSuffixLoop x useLe m j (j + 1) 1 1
    else
      if a > b then
        maximalSuffixLoop x useLe m ms (j + k) 1 (j + k - ms)
      else if a == b then
        if k != p then
          maximalSuffixLoop x useLe m ms j (k + 1) p
        else
          maximalSuffixLoop x useLe m ms (j + p) 1 p
      else
        maximalSuffixLoop x useLe m j (j + 1) 1 1
def maximalSuffix (x : ByteArray) (useLe : Bool) : (Int × Int) :=
  let m : Int := x.size
  maximalSuffixLoop x useLe m (-1) 0 1 1
partial def twoWayForward1 (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) : Int :=
  if j >= n then
    j
  else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
    twoWayForward1 haystack needle i n (j + 1)
  else
    j
partial def twoWayBackward1 (haystack needle : ByteArray) (i : Nat) (mem : Int) (j : Int) : Int :=
  if j <= mem then
    j
  else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
    twoWayBackward1 haystack needle i mem (j - 1)
  else
    j
partial def twoWayForward2 (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) : Int :=
  if j >= n then
    j
  else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
    twoWayForward2 haystack needle i n (j + 1)
  else
    j
partial def twoWayBackward2 (haystack needle : ByteArray) (i : Nat) (j : Int) : Int :=
  if j < 0 then
    j
  else if haystack[i + Int.toNat j]! == needle[Int.toNat j]! then
    twoWayBackward2 haystack needle i (j - 1)
  else
    j
partial def twoWayShortLoop (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) (mem : Int) : Option Nat :=
  if i > maxStart then
    none
  else
    let j0 := max (Int.ofNat msNat) mem + 1
    let j := twoWayForward1 haystack needle i n j0
    if j >= n then
      let j2 := twoWayBackward1 haystack needle i mem (Int.ofNat msNat)
      if j2 <= mem then
        some i
      else
        let nextI := i + pNat
        let nextMem := Int.ofNat (n - pNat - 1)
        twoWayShortLoop haystack needle start maxStart msNat pNat n nextI nextMem
    else
      let shift := Int.toNat (j - Int.ofNat msNat)
      twoWayShortLoop haystack needle start maxStart msNat pNat n (i + shift) (-1)
partial def twoWayLongLoop (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) : Option Nat :=
  if i > maxStart then
    none
  else
    let j := twoWayForward2 haystack needle i n (Int.ofNat (msNat + 1))
    if j >= n then
      let j2 := twoWayBackward2 haystack needle i (Int.ofNat msNat)
      if j2 < 0 then
        some i
      else
        let nextI := i + pNat
        twoWayLongLoop haystack needle start maxStart msNat pNat n nextI
    else
      let shift := Int.toNat (j - Int.ofNat msNat)
      twoWayLongLoop haystack needle start maxStart msNat pNat n (i + shift)
def twoWaySearch (haystack : ByteArray) (needle : ByteArray) (start : Nat) : Option Nat :=
  let n := needle.size
  let h := haystack.size
  if n == 0 then
    some start
  else if h < n || start + n > h then
    none
  else
    let (ms1, p1) := maximalSuffix needle true
    let (ms2, p2) := maximalSuffix needle false
    let (ms, p) := if ms1 > ms2 then (ms1, p1) else (ms2, p2)
    let msNat := Int.toNat ms
    let pNat := Int.toNat p
    let maxStart := h - n
    let rec prefixEqual (i : Nat) : Bool :=
      if ms < 0 then true
      else if i > msNat then true
      else if i + pNat >= n then false
      else if needle[i]! == needle[i + pNat]! then
        prefixEqual (i + 1)
      else
        false
    let shortPeriod := prefixEqual 0
    if shortPeriod then
      twoWayShortLoop haystack needle start maxStart msNat pNat n start (-1)
    else
      twoWayLongLoop haystack needle start maxStart msNat pNat n start
partial def findPatternInBytes (haystack : ByteArray) (needle : ByteArray) (start : Nat) : Option Nat :=
  twoWaySearch haystack needle start
partial def findLastPatternInBytes (haystack : ByteArray) (needle : ByteArray) : Option Nat :=
  let n := needle.size
  let h := haystack.size
  if n == 0 then
    some 0
  else if h < n then
    none
  else
    let maxStart := h - n
    let rec loop (i : Nat) (last : Option Nat) : Option Nat :=
      if i > maxStart then last
      else
        match findPatternInBytes haystack needle i with
        | some idx =>
            if idx > maxStart then last
            else loop (idx + 1) (some idx)
        | none => last
    loop 0 none
/-- Search forward for a byte pattern from a given offset -/
partial def searchNext (t : ViE.PieceTree) (pt : ViE.PieceTable) (pattern : ByteArray) (startOffset : Nat) (chunkSize : Nat)
  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat)
  : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
  if pattern.size == 0 then
    (none, cache, order)
  else
    let total := length t
    if startOffset >= total then
      (none, cache, order)
    else
      if pattern.size < 3 || !useBloom then
        let chunkLen := max chunkSize pattern.size
        let overlap := pattern.size - 1
        let rec loop (offset : Nat) : Option Nat :=
          if offset >= total then none
          else
            let remaining := total - offset
            let readLen := min chunkLen remaining
            if readLen < pattern.size then
              none
            else
              let bytes := getBytes t offset readLen pt
              match findPatternInBytes bytes pattern 0 with
              | some idx => some (offset + idx)
              | none =>
                if offset + readLen >= total then none
                else
                  let nextOffset := offset + (readLen - overlap)
                  loop nextOffset
        (loop startOffset, cache, order)
      else
        let hashes := patternTrigramHashes pattern
        let rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)
          (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
          : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
          if baseOffset + length node <= startOffset then
            (none, cache, order)
          else
            match node with
            | ViE.PieceTree.empty => (none, cache, order)
            | ViE.PieceTree.leaf _ _ _ =>
                let relStart := if startOffset > baseOffset then startOffset - baseOffset else 0
                let remain := length node - relStart
                if remain < pattern.size then
                  (none, cache, order)
                else
                  match node with
                  | ViE.PieceTree.leaf pieces _ m =>
                      let (bits, cache, order) :=
                        if bloomIsEmpty m.bits then
                          leafBloomBitsWithCache pieces pt baseOffset cache order cacheMax
                        else
                          (m.bits, cache, order)
                      if !bloomMayContain bits hashes then
                        (none, cache, order)
                      else
                        let bytes := getBytes node relStart remain pt
                        match findPatternInBytes bytes pattern 0 with
                        | some idx => (some (baseOffset + relStart + idx), cache, order)
                        | none => (none, cache, order)
                  | _ => (none, cache, order)
            | ViE.PieceTree.internal children _ _ =>
                let rec loop (i : Nat) (offset : Nat)
                  (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
                  : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
                  if i >= children.size then
                    (none, cache, order)
                  else
                    let child := children[i]!
                    let childLen := length child
                    let childEnd := offset + childLen
                    if childEnd <= startOffset then
                      loop (i + 1) childEnd cache order
                    else
                      match searchNode child offset cache order with
                      | (some res, cache, order) => (some res, cache, order)
                      | (none, cache, order) => loop (i + 1) childEnd cache order
                loop 0 baseOffset cache order
        searchNode t 0 cache order
/-- Search backward for a byte pattern ending before startExclusive -/
partial def searchPrev (t : ViE.PieceTree) (pt : ViE.PieceTable) (pattern : ByteArray) (startExclusive : Nat) (chunkSize : Nat)
  (useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat)
  : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
  if pattern.size == 0 then
    (none, cache, order)
  else
    let total := length t
    let end0 := min startExclusive total
    if end0 == 0 then
      (none, cache, order)
    else if pattern.size < 3 || !useBloom then
      let chunkLen := max chunkSize pattern.size
      let overlap := pattern.size - 1
      let rec loop (endOffset : Nat) : Option Nat :=
        if endOffset == 0 then none
        else
          let start := if endOffset > chunkLen then endOffset - chunkLen else 0
          let readLen := endOffset - start
          if readLen < pattern.size then
            if start == 0 then none else loop (start + overlap)
          else
            let bytes := getBytes t start readLen pt
            match findLastPatternInBytes bytes pattern with
            | some idx =>
                let pos := start + idx
                if pos < endOffset then some pos else none
            | none =>
                if start == 0 then none else loop (start + overlap)
      (loop end0, cache, order)
    else
      let hashes := patternTrigramHashes pattern
      let rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)
        (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
        : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
        if baseOffset >= end0 then
          (none, cache, order)
        else
          match node with
          | ViE.PieceTree.empty => (none, cache, order)
          | ViE.PieceTree.leaf _ _ _ =>
              let relEnd := min (end0 - baseOffset) (length node)
              if relEnd < pattern.size then
                (none, cache, order)
              else
                match node with
                | ViE.PieceTree.leaf pieces _ m =>
                    let (bits, cache, order) :=
                      if bloomIsEmpty m.bits then
                        leafBloomBitsWithCache pieces pt baseOffset cache order cacheMax
                      else
                        (m.bits, cache, order)
                    if !bloomMayContain bits hashes then
                      (none, cache, order)
                    else
                      let bytes := getBytes node 0 relEnd pt
                      match findLastPatternInBytes bytes pattern with
                      | some idx => (some (baseOffset + idx), cache, order)
                      | none => (none, cache, order)
                | _ => (none, cache, order)
          | ViE.PieceTree.internal children _ _ =>
              let spans : Array (ViE.PieceTree × Nat) := Id.run do
                let mut acc : Array (ViE.PieceTree × Nat) := #[]
                let mut offset := baseOffset
                for child in children do
                  acc := acc.push (child, offset)
                  offset := offset + length child
                return acc
              let rec loop (i : Nat)
                (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
                : (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=
                if i >= spans.size then
                  (none, cache, order)
                else
                  let j := spans.size - 1 - i
                  let (child, childOffset) := spans[j]!
                  if childOffset >= end0 then
                    loop (i + 1) cache order
                  else
                    match searchNode child childOffset cache order with
                    | (some res, cache, order) =>
                        if res < end0 then (some res, cache, order) else loop (i + 1) cache order
                    | (none, cache, order) => loop (i + 1) cache order
              loop 0 cache order
      searchNode t 0 cache order

/-- Bloom filter bit size for trigram indexing. -/
def BloomBits : Nat := 4096
/-- Bloom filter byte size. -/
def BloomBytes : Nat := BloomBits / 8
/-- Build full bloom bits for leaf nodes (startup cost). -/
def BloomBuildLeafBits : Bool := false
/-- Search metadata for a piece tree node. -/
structure SearchBloom where
  bits : ByteArray
  prefixBytes : Array UInt8
  suffixBytes : Array UInt8
  deriving Inhabited
def SearchBloom.empty : SearchBloom := {
  bits := ByteArray.mk (Array.replicate BloomBytes (0 : UInt8)),
  prefixBytes := #[],
  suffixBytes := #[]
}

instance : Repr SearchBloom where
  reprPrec sb _ :=
    s!"SearchBloom(bits={sb.bits.size}, prefix={sb.prefixBytes}, suffix={sb.suffixBytes})"

  | leaf (pieces : Array Piece) (stats : Stats)
  | internal (children : Array PieceTree) (stats : Stats)

  | leaf (pieces : Array Piece) (stats : Stats) (searchMeta : SearchBloom)
  | internal (children : Array PieceTree) (stats : Stats) (searchMeta : SearchBloom)

import ViE.Key.Handler

  | .searchForward => ViE.Key.handleSearchInput state k
  | .searchBackward => ViE.Key.handleSearchInput state k

def cmdBloom (args : List String) (state : EditorState) : IO EditorState := do
  let (direction, pattern) :=
    match args with
    | [] => (SearchDirection.forward, "")
    | [p] =>
        if p.startsWith "/" then
          (SearchDirection.forward, (p.drop 1).toString)
        else if p.startsWith "?" then
          (SearchDirection.backward, (p.drop 1).toString)
        else
          (SearchDirection.forward, p)
    | p :: rest =>
        let full := String.intercalate " " (p :: rest)
        if full.startsWith "/" then
          (SearchDirection.forward, (full.drop 1).toString)
        else if full.startsWith "?" then
          (SearchDirection.backward, (full.drop 1).toString)
        else
          (SearchDirection.forward, full)
  if pattern.isEmpty then
    return { state with message := "Empty search pattern" }
  else
    let s' := ViE.startOrUpdateSearch state pattern direction true
    let s'' := ViE.findNextMatch s' (some direction)
    return s''

def cmdNoHighlight (_ : List String) (state : EditorState) : IO EditorState :=
  return { state with searchState := none, message := "search highlight cleared" }

  ("refresh", cmdReload)

  ("refresh", cmdReload),
  ("bloom", cmdBloom),
  ("nohl", cmdNoHighlight),
  ("noh", cmdNoHighlight)

      if h : real < wg.workspaces.size then

      if real < wg.workspaces.size then

      if h : real < state.workgroups.size then

      if real < state.workgroups.size then

import ViE.State.Search
import ViE.Data.PieceTable.Tree

partial def collectMatchesInBytes (haystack : ByteArray) (needle : ByteArray) : Array (Nat × Nat) :=
  let n := needle.size
  let h := haystack.size
  if n == 0 || h < n then
    #[]
  else
    let rec loop (i : Nat) (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=
      if i + n > h then
        acc
      else
        match ViE.PieceTree.findPatternInBytes haystack needle i with
        | some idx =>
            if idx + n > h then
              acc
            else
              loop (idx + n) (acc.push (idx, idx + n))
        | none => acc
    loop 0 #[]
partial def collectMatchesInPieceTable (pt : PieceTable) (pattern : ByteArray) : Array (Nat × Nat) :=
  let n := pattern.size
  if n == 0 then
    #[]
  else
    let total := pt.tree.length
    let rec loop (offset : Nat)
      (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)
      (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=
      if offset >= total then
        acc
      else
        let (res, cache', order') :=
          ViE.PieceTree.searchNext pt.tree pt pattern offset ViE.searchChunkSize false cache order 0
        match res with
        | some idx =>
            if idx + n > total then
              acc
            else
              loop (idx + n) cache' order' (acc.push (idx, idx + n))
        | none => acc
    loop 0 Lean.RBMap.empty #[] #[]
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 parseSubstitute (cmd : String) : Option (Bool × String × String × String) :=
  let (isGlobal, rest) :=
    if cmd.startsWith "%s/" then
      (true, (cmd.drop 3).toString)
    else if cmd.startsWith "s/" then
      (false, (cmd.drop 2).toString)
    else
      (false, "")
  if rest.isEmpty then
    none
  else
    let parts := rest.splitOn "/"
    match parts with
    | old :: new :: flagsParts =>
        let flags := String.intercalate "/" flagsParts
        some (isGlobal, old, new, flags)
    | _ => none
def parseGlobal (cmd : String) : Option (Bool × String × String) :=
  if cmd.startsWith "g/" || cmd.startsWith "v/" then
    let isInvert := cmd.startsWith "v/"
    let rest := (cmd.drop 2).toString
    let parts := rest.splitOn "/"
    match parts with
    | pat :: cmdParts =>
        let subcmd := String.intercalate "/" cmdParts
        some (isInvert, pat, (subcmd.trimAscii).toString)
    | _ => none
  else
    none
def lineRangeWithNewline (pt : PieceTable) (row : Nat) : Option (Nat × Nat) :=
  match pt.getLineRange row with
  | some (startOff, len) =>
      let endOff := startOff + len
      if endOff < pt.tree.length then
        let b := ViE.PieceTree.getBytes pt.tree endOff 1 pt
        if b.size == 1 && b[0]! == (UInt8.ofNat 10) then
          some (startOff, len + 1)
        else
          some (startOff, len)
      else
        some (startOff, len)
  | none => none

def collectMatchesInLine (pt : PieceTable) (row : Nat) (pattern : ByteArray) : Array (Nat × Nat) :=
  match pt.getLineRange row with
  | some (startOff, len) =>
      let bytes := ViE.PieceTree.getBytes pt.tree startOff len pt
      let localMatches := collectMatchesInBytes bytes pattern
      localMatches.map (fun (s, e) => (startOff + s, startOff + e))
  | none => #[]
def execGlobal (cmd : String) (state : EditorState) : EditorState :=
  match parseGlobal cmd with
  | none => { state with message := s!"Invalid global: {cmd}" }
  | some (isInvert, pat, subcmd) =>
      if pat.isEmpty then
        { state with message := "Empty global pattern" }
      else
        let buf := state.getActiveBuffer
        let cursor := state.getCursor
        let cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0
        let patBytes := pat.toUTF8
        let lineCount := buf.lineCount
        let matchingRows : Array Nat := Id.run do
          let mut rows : Array Nat := #[]
          for row in [0:lineCount] do
            let hasMatch := (collectMatchesInLine buf.table row patBytes).size > 0
            if (if isInvert then !hasMatch else hasMatch) then
              rows := rows.push row
          return rows
        if subcmd == "d" then
          let ranges : Array (Nat × Nat) := Id.run do
            let mut acc : Array (Nat × Nat) := #[]
            for row in matchingRows do
              match lineRangeWithNewline buf.table row with
              | some (startOff, len) => acc := acc.push (startOff, startOff + len)
              | none => pure ()
            return acc
          let newTable := buf.table.applyDeletions cursorOffset ranges
          let newBuf := { buf with table := newTable, dirty := true }
          state.updateActiveBuffer (fun _ => newBuf)
        else if subcmd.startsWith "s/" then
          match parseSubstitute subcmd with
          | none => { state with message := s!"Invalid substitute: {subcmd}" }
          | some (_isGlobal, old, new, flags) =>
              if old.isEmpty then
                { state with message := "Empty substitute pattern" }
              else
                let doGlobal := flags.contains 'g'
                let oldBytes := old.toUTF8
                let matches1 : Array (Nat × Nat) := Id.run do
                  let mut acc : Array (Nat × Nat) := #[]
                  for row in matchingRows do
                    let lineMatches := collectMatchesInLine buf.table row oldBytes
                    if doGlobal then
                      acc := acc.append lineMatches
                    else
                      match lineMatches[0]? with
                      | some first => acc := acc.push first
                      | none => pure ()
                  return acc
                let newTable := buf.table.applyReplacements cursorOffset matches1 new
                let newBuf := { buf with table := newTable, dirty := true }
                state.updateActiveBuffer (fun _ => newBuf)
        else
          { state with message := s!"Unsupported global subcommand: {subcmd}" }
def execSubstitute (cmd : String) (state : EditorState) : EditorState :=
  match parseSubstitute cmd with
  | none => { state with message := s!"Invalid substitute: {cmd}" }
  | some (isGlobal, old, new, flags) =>
      if old.isEmpty then
        { state with message := "Empty substitute pattern" }
      else
        let doGlobal := flags.contains 'g'
        let buf := state.getActiveBuffer
        let cursor := state.getCursor
        let cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0
        let patBytes := old.toUTF8
        let matches1 :=
          if isGlobal then
            if doGlobal then
              collectMatchesInPieceTable buf.table patBytes
            else
              Id.run do
                let lineCount := buf.lineCount
                let mut acc : Array (Nat × Nat) := #[]
                for row in [0:lineCount] do
                  match buf.table.getLineRange row with
                  | some (startOff, len) =>
                      let bytes := ViE.PieceTree.getBytes buf.table.tree startOff len buf.table
                      match (collectMatchesInBytes bytes patBytes)[0]? with
                      | some (s, e) => acc := acc.push (startOff + s, startOff + e)
                      | none => pure ()
                  | none => pure ()
                return acc
          else
            match buf.table.getLineRange cursor.row.val with
            | some (startOff, len) =>
                let bytes := ViE.PieceTree.getBytes buf.table.tree startOff len buf.table
                let localMatches := collectMatchesInBytes bytes patBytes
                localMatches.map (fun (s, e) => (startOff + s, startOff + e))
            | none => #[]
        let matches2 :=
          if doGlobal || isGlobal then
            matches1
          else
            match matches1[0]? with
            | some first => #[first]
            | none => #[]
        let newTable := buf.table.applyReplacements cursorOffset matches2 new
        let newBuf := { buf with table := newTable, dirty := true }
        state.updateActiveBuffer (fun _ => newBuf)

  if fullCmd.startsWith "s/" || fullCmd.startsWith "%s/" then
    return execSubstitute fullCmd state
  if fullCmd.startsWith "g/" || fullCmd.startsWith "v/" then
    return execGlobal fullCmd state

    let stateAfterTimeout := ViE.maybeRunIncrementalSearch stateAfterTimeout currentTime

  let config := ViE.defaultConfig

  match s_x.clipboard with
  | some reg =>
      assertEqual "x register kind" RegisterKind.charwise reg.kind
      assertEqual "x register text" "x" reg.text
  | none => assertEqual "x register set" true false

  match s_dw.clipboard with
  | some reg =>
      assertEqual "dw register kind" RegisterKind.charwise reg.kind
      assertEqual "dw register text" "hello " reg.text
  | none => assertEqual "dw register set" true false

  match s_dd.clipboard with
  | some reg =>
      assertEqual "dd register kind" RegisterKind.linewise reg.kind
      assertEqual "dd register text" "line2\n" reg.text
  | none => assertEqual "dd register set" true false

  let s_indent ← runKeys s0 ([Key.char 'i'] ++ keys "  indented\nx" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char 'y', Key.char 'y', Key.char 'j', Key.char 'p'])
  assertCursor "linewise paste moves to first non-blank" s_indent 2 2
  -- paste should not overwrite register
  let s_reg0 ← runKeys s0 ([Key.char 'i'] ++ keys "one\ntwo" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char 'y', Key.char 'y'])
  let regBefore := s_reg0.clipboard
  let s_regP ← runKeys s_reg0 [Key.char 'j', Key.char 'p']
  match (regBefore, s_regP.clipboard) with
  | (some before, some after) =>
      assertEqual "paste keeps register kind" before.kind after.kind
      assertEqual "paste keeps register text" before.text after.text
  | _ => assertEqual "paste keeps register" true false

  -- charwise y/p from normal mode
  let s_char0 ← runKeys s0 ([Key.char 'i'] ++ keys "hello" ++ [Key.esc] ++ [Key.char '0'])
  let s_charY ← runKeys s_char0 [Key.char 'v', Key.char 'l', Key.char 'y']
  let s_charP ← runKeys s_charY [Key.char '$', Key.char 'p']
  assertBuffer "charwise paste in normal mode" s_charP "hellohe"
  assertCursor "charwise paste cursor at end" s_charP 0 6
  let s_charP2 ← runKeys s_charY [Key.char '0', Key.char 'P']
  assertBuffer "charwise P pastes before cursor" s_charP2 "hehello"
  assertCursor "charwise P cursor at end" s_charP2 0 1

  match s_v.clipboard with
  | some reg =>
      assertEqual "visual d register kind" RegisterKind.charwise reg.kind
      assertEqual "visual d register text" "hi" reg.text
  | none => assertEqual "visual d register set" true false

  assertBuffer "visual y yanks selection" s_vyp "highlight me\nhighlight"

  assertBuffer "visual y yanks selection" s_vyp "highlight mehighlight"
  let s_char0 ← runKeys s0 ([Key.char 'i'] ++ keys "abc" ++ [Key.esc] ++ [Key.char '0'])
  let s_charY ← runKeys s_char0 [Key.char 'l', Key.char 'v', Key.char 'y']
  let s_charP ← runKeys s_charY [Key.char '$', Key.char 'p']
  assertBuffer "charwise paste appends" s_charP "abcb"
  assertCursor "charwise paste cursor at end" s_charP 0 3
  let s_charP2 ← runKeys s_charY [Key.char '0', Key.char 'P']
  assertBuffer "charwise P inserts before" s_charP2 "babc"
  assertCursor "charwise P cursor at end" s_charP2 0 0
  -- visual block yank/paste cursor position
  let s_blk0 ← runKeys s0 ([Key.char 'i'] ++ keys "abcd\nefgh" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char '0'])
  let s_blkY ← runKeys s_blk0 [Key.char 'l', Key.char 'V', Key.char 'l', Key.char 'j', Key.char 'y']
  let s_blkP ← runKeys s_blkY [Key.char 'g', Key.char 'g', Key.char '0', Key.char 'p']
  assertBuffer "visual block y/p inserts block" s_blkP "abcbcd\nefgfgh"
  assertCursor "visual block paste cursor at block start" s_blkP 0 1
  let s_blkP2 ← runKeys s_blkY [Key.char 'g', Key.char 'g', Key.char '0', Key.char 'P']
  assertBuffer "visual block P inserts block" s_blkP2 "bcabcd\nfgefgh"
  assertCursor "visual block P cursor at block start" s_blkP2 0 0
  let s_blkD0 ← runKeys s0 ([Key.char 'i'] ++ keys "abcd\nefgh" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char '0'])
  let s_blkD ← runKeys s_blkD0 [Key.char 'l', Key.char 'V', Key.char 'l', Key.char 'j', Key.char 'd']
  assertBuffer "visual block d deletes block" s_blkD "ad\neh"
  match s_blkD.clipboard with
  | some reg =>
      assertEqual "visual block d register kind" RegisterKind.blockwise reg.kind
      assertEqual "visual block d register text" "bc\nfg" reg.text
  | none => assertEqual "visual block d register set" true false
  -- linewise yank/paste (via yy + P)
  let s_line0 ← runKeys s0 ([Key.char 'i'] ++ keys "aa\nbb\ncc" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g'])
  let s_lineY ← runKeys s_line0 [Key.char 'y', Key.char 'y']
  let s_lineP ← runKeys s_lineY [Key.char 'j', Key.char 'P']
  assertBuffer "linewise paste above keeps lines" s_lineP "aa\naa\nbb\ncc"

  let s_lineP2 ← runKeys s_lineY [Key.char 'j', Key.char 'p']
  assertBuffer "linewise paste below keeps lines" s_lineP2 "aa\nbb\naa\ncc"

def testSearch : IO Unit := do
  IO.println "  Testing Search..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "hello world\nhello again\n" ++ [Key.esc])
  let s2 ← runKeys s1 ([Key.char '/'] ++ keys "hello" ++ [Key.enter])
  assertCursor "/hello finds first match" s2 0 0
  let s3 ← runKeys s2 [Key.char 'n']
  assertCursor "n finds next match" s3 1 0
  let s4 ← runKeys s3 [Key.char 'N']
  assertCursor "N finds previous match" s4 0 0
  let s5 ← runKeys s4 ([Key.char '?'] ++ keys "world" ++ [Key.enter])
  assertCursor "?world searches backward" s5 0 6
def testCommandSubstitute : IO Unit := do
  IO.println "  Testing Command Substitute..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "foo bar\nfoo baz\nbar foo\n" ++ [Key.esc] ++ keys "gg0")
  let s2 ← runKeys s1 ([Key.char ':'] ++ keys "s/foo/xxx/" ++ [Key.enter])
  assertBuffer ":s replaces first match on current line" s2 "xxx bar\nfoo baz\nbar foo\n"
  let s3 := ViE.initialState
  let s4 ← runKeys s3 ([Key.char 'i'] ++ keys "foo foo\nfoo foo\n" ++ [Key.esc] ++ keys "gg0")
  let s5 ← runKeys s4 ([Key.char ':'] ++ keys "%s/foo/yyy/" ++ [Key.enter])
  assertBuffer ":%s replaces first match per line" s5 "yyy foo\nyyy foo\n"
  let s6 := ViE.initialState
  let s7 ← runKeys s6 ([Key.char 'i'] ++ keys "foo bar\nfoo baz\nbar foo\n" ++ [Key.esc] ++ keys "gg0")
  let s8 ← runKeys s7 ([Key.char ':'] ++ keys "%s/foo/yyy/g" ++ [Key.enter])
  assertBuffer ":%s with g replaces all matches" s8 "yyy bar\nyyy baz\nbar yyy\n"

def testCommandGlobal : IO Unit := do
  IO.println "  Testing Command Global..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "a\nfoo1\nb\nfoo2\n" ++ [Key.esc] ++ keys "gg0")
  let s2 ← runKeys s1 ([Key.char ':'] ++ keys "g/foo/ d" ++ [Key.enter])
  assertBuffer ":g/pat/ d deletes matching lines" s2 "a\nb\n"
  let s3 := ViE.initialState
  let s4 ← runKeys s3 ([Key.char 'i'] ++ keys "foo foo\nbar foo\nfoo bar\n" ++ [Key.esc] ++ keys "gg0")
  let s5 ← runKeys s4 ([Key.char ':'] ++ keys "g/foo/ s/foo/xxx/" ++ [Key.enter])
  assertBuffer ":g/pat/ s replaces first match per line" s5 "xxx foo\nbar xxx\nxxx bar\n"
  let s6 := ViE.initialState
  let s7 ← runKeys s6 ([Key.char 'i'] ++ keys "keep1\nfoo\nkeep2\n" ++ [Key.esc] ++ keys "gg0")
  let s8 ← runKeys s7 ([Key.char ':'] ++ keys "v/foo/ d" ++ [Key.enter])
  assertBuffer ":v/pat/ d deletes non-matching lines" s8 "foo\n"
def testCommandBloom : IO Unit := do
  IO.println "  Testing Command Bloom..."
  let s0 := ViE.initialState
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys "hello bloom\nbloom hello\n" ++ [Key.esc] ++ keys "gg0")
  let s2 ← runKeys s1 ([Key.char ':'] ++ keys "bloom /bloom" ++ [Key.enter])
  assertCursor ":bloom moves to first match" s2 0 6
  let s3 ← runKeys s2 ([Key.char ':'] ++ keys "bloom /nomatch" ++ [Key.enter])
  assertEqual ":bloom not found message" "Pattern not found: nomatch" s3.message

  testSearch
  testCommandSubstitute
  testCommandGlobal
  testCommandBloom