[[lean_exe]]
name = "tree-stats"
root = "Test.TreeStats"

        { ws with layout := newLayout, activeWindowId := newActiveId }

        { ws with layout := newLayout, activeWindowId := newActiveId } |>.pruneFloatingWindows

    let activeWasFloating := ws.isFloatingWindow activeId
    let (activeRowOff, activeColOff) := ws.getFloatingWindowOffset activeId

    { ws with layout := updateLayout ws.layout, nextWindowId := nextId + 1 }

    let ws' := { ws with layout := updateLayout ws.layout, nextWindowId := nextId + 1 }
    let ws' :=
      if activeWasFloating then
        (ws'.setWindowFloating nextId true).setFloatingWindowOffset nextId activeRowOff activeColOff
      else
        ws'
    ws'.pruneFloatingWindows

def nudgeActiveFloatingWindow (state : EditorState) (dir : Direction) (step : Int := 1) : EditorState :=
  let ws := state.getCurrentWorkspace
  let activeId := ws.activeWindowId
  if !ws.isFloatingWindow activeId then
    { state with message := "active window is not floating" }
  else
    match ws.findFloatingSubtree activeId with
    | none => { state with message := "floating window subtree not found" }
    | some subtree =>
      let ids := ViE.Window.getWindowIds subtree
      let dRow : Int :=
        match dir with
        | .up => -step
        | .down => step
        | _ => 0
      let dCol : Int :=
        match dir with
        | .left => -step
        | .right => step
        | _ => 0
      let s' := state.updateCurrentWorkspace fun ws =>
        ids.foldl (fun acc wid => acc.adjustFloatingWindowOffset wid dRow dCol) ws
      { s' with dirty := true, message := "floating window moved" }

  let (h, w) := state.getActiveWindowBounds
  -- Active window height already excludes the global status line.
  let linesInView := if h > 0 then h else 1

  let (h, w) := state.getActiveWindowScrollBounds
  let linesInView := if h > 1 then h - 1 else 1

      let newScrollRow : Row := ⟨cursor.row.val - (linesInView - 1)⟩

      let newScrollRow : Row := ⟨cursor.row.val - linesInView + 1⟩

      let newScrollCol : Col := ⟨sCol.val + colsInView - 1⟩

      let newScrollCol : Col := ⟨cursor.col.val - colsInView + 1⟩

import ViE.State
import ViE.Terminal
import ViE.Config
import ViE.Unicode
import ViE.Color
namespace ViE.UI
open ViE
/-- 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 overlapsByteRange (r : Nat × Nat) (byteStart byteEnd : Nat) : Bool :=
  let (s, e) := r
  byteStart < e && byteEnd > s
def activeMatchRange (hitRanges : Array (Nat × Nat)) (cursorByte : Option Nat) : Option (Nat × Nat) :=
  match cursorByte with
  | none => none
  | some cb =>
      let rec loop (i : Nat) : Option (Nat × Nat) :=
        if i >= hitRanges.size then
          none
        else
          let m := hitRanges[i]!
          let (s, e) := m
          if s <= cb && cb < e then
            some m
          else
            loop (i + 1)
      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 } }
/-- Pad a string on the left with spaces until it reaches the given width. -/
def leftPad (s : String) (width : Nat) : String :=
  if s.length >= width then s
  else "".pushn ' ' (width - s.length) ++ s
/-- Take characters from substring until visual width limit is reached. -/
def takeVisual (s : Substring.Raw) (width : Nat) : String :=
  Unicode.takeByDisplayWidth s width
/-- Render the current editor state to the terminal. -/
def render (state : EditorState) : IO EditorState := do
  if !state.dirty then return state
  -- Start building the frame buffer
  let mut buffer : Array String := #[]
  buffer := buffer.push Terminal.hideCursorStr
  buffer := buffer.push Terminal.homeCursorStr
  let (rows, cols) ← Terminal.getWindowSize
  let ws := state.getCurrentWorkspace
  let getBuffer (st : EditorState) (id : Nat) : FileBuffer :=
    let ws := st.getCurrentWorkspace
    ws.buffers.find? (fun b => b.id == id) |>.getD initialFileBuffer
  let rec renderLayout (l : Layout) (st : EditorState) (r c h w : Nat) : (Array String × EditorState) := Id.run do
    match l with
    | Layout.window id view =>
      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 workH := if h > 0 then h - 1 else 0
      let buf := getBuffer st view.bufferId
      let mut currentSt := st
      let mut winBuf : Array String := #[]
      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
      for i in [0:workH] do
        let lineIdx : Row := ⟨view.scrollRow.val + i⟩
        let screenRow := r + i
        -- Position cursor for this line
        winBuf := winBuf.push (Terminal.moveCursorStr screenRow c)
        if lineIdx.val < FileBuffer.lineCount buf then
           -- Check cache
           let lnWidth := if st.config.showLineNumbers then 4 else 0
           let availableWidth := if w > lnWidth then w - lnWidth else 0
           let cachedLine := buf.cache.find lineIdx
           let cachedRaw := buf.cache.findRaw lineIdx
           let cachedIdx := buf.cache.findIndex lineIdx
           let lineStr := cachedRaw.getD (getLineFromBuffer buf lineIdx |>.getD "")
           let lineIndex := cachedIdx.getD (ViE.Unicode.buildDisplayByteIndex lineStr)
           let (displayLine, nextSt) := match cachedLine with
             | some (s, cachedScrollCol, cachedWidth) =>
               if cachedScrollCol == view.scrollCol.val && cachedWidth == availableWidth then
                 (s, currentSt)
               else
                 -- Cache miss; fall through to recompute.
                 match getLineFromBuffer buf lineIdx with
                 | some lineStr =>
                   let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val
                   let dl := takeVisual sub availableWidth
                   let cache := match cachedRaw, cachedIdx with
                     | some raw, some _ =>
                       if raw == lineStr then
                         buf.cache
                       else
                         (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                     | _, _ =>
                       (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                   let cache := (cache.update lineIdx dl view.scrollCol.val availableWidth).updateRaw lineIdx lineStr
                   let updatedBuf := { buf with cache := cache }
                   let s' := currentSt.updateCurrentWorkspace fun ws =>
                     { ws with buffers := ws.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
                   (dl, s')
                 | none => ("", currentSt)
             | none =>
               if let some lineStr := getLineFromBuffer buf lineIdx then
                 let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val
                 let dl := takeVisual sub availableWidth
                 let cache := match cachedRaw, cachedIdx with
                   | some raw, some _ =>
                     if raw == lineStr then
                       buf.cache
                     else
                       (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                   | _, _ =>
                     (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                 -- Update cache in currentSt
                 let cache := (cache.update lineIdx dl view.scrollCol.val availableWidth).updateRaw lineIdx lineStr
                 let updatedBuf := { buf with cache := cache }
                 let s' := currentSt.updateCurrentWorkspace fun ws =>
                   { ws with buffers := ws.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
                 (dl, s')
               else ("", currentSt)
           currentSt := nextSt
           if st.config.showLineNumbers then
             winBuf := winBuf.push s!"{leftPad (toString (lineIdx.val + 1)) 3} "
           let isVisual := st.mode == Mode.visual || st.mode == Mode.visualBlock
           let selRange := if isVisual then st.selectionStart else none
           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
           let needsStyled := selRange.isSome || !searchMatches.isEmpty
           if !needsStyled then
             winBuf := winBuf.push displayLine
           else
             let mut styleActive := false
             let chars := displayLine.toList
             let mut dispIdx := 0
             let cursorByte :=
               if lineIdx == view.cursor.row then
                 some (ViE.Unicode.displayColToByteOffsetFromIndex lineIndex view.cursor.col.val)
               else
                 none
             let activeMatch := activeMatchRange searchMatches cursorByte
             for ch in chars do
                let w := Unicode.charWidth ch
                let colVal := view.scrollCol.val + dispIdx
                let byteStart := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex colVal
                let byteEnd := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex (colVal + w)
                let isSelected :=
                  st.isInSelection lineIdx ⟨colVal⟩ ||
                  (w > 1 && st.isInSelection lineIdx ⟨colVal + 1⟩)
                let isMatched :=
                  searchMatches.any (fun m => overlapsByteRange m byteStart byteEnd)
                let isActiveMatched :=
                  match activeMatch with
                  | some m => overlapsByteRange m byteStart byteEnd
                  | none => false
                if isSelected then
                  if !styleActive then
                    winBuf := winBuf.push "\x1b[7m" -- Inverse video
                    styleActive := true
                else if isMatched then
                  if !styleActive then
                    if isActiveMatched then
                      winBuf := winBuf.push st.config.searchHighlightCursorStyle
                    else
                      winBuf := winBuf.push st.config.searchHighlightStyle
                    styleActive := true
                else if styleActive then
                  winBuf := winBuf.push "\x1b[0m"
                  styleActive := false
                winBuf := winBuf.push ch.toString
                dispIdx := dispIdx + w
             if styleActive then winBuf := winBuf.push "\x1b[0m"
        else
           winBuf := winBuf.push st.config.emptyLineMarker
        -- Clear the rest of the line
        winBuf := winBuf.push Terminal.clearLineStr
      let statusRow := r + workH
      winBuf := winBuf.push (Terminal.moveCursorStr statusRow c)
      let fileName := buf.filename.getD "[No Name]"
      let modeStr := if id == currentSt.getCurrentWorkspace.activeWindowId then s!"-- {st.mode} --" else "--"
      let eolMark := if buf.missingEol then " [noeol]" else ""
      let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{id} B:{view.bufferId}] [{st.getCurrentWorkgroup.name}] {st.getCurrentWorkspace.name}"
      winBuf := winBuf.push st.config.statusBarStyle
      winBuf := winBuf.push statusStr.trimAscii.toString
      winBuf := winBuf.push Terminal.clearLineStr
      winBuf := winBuf.push st.config.resetStyle
      (winBuf, currentSt)
    | Layout.hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      let (leftStr, st') := renderLayout left st r c h leftW
      -- Draw vertical separator
      let mut sepStr : Array String := #[]
      if w > leftW then
        let sepCol := c + leftW
        for i in [0:h] do
           sepStr := sepStr.push (Terminal.moveCursorStr (r + i) sepCol)
           sepStr := sepStr.push st.config.vSplitStr
      let (rightStr, st'') := renderLayout right st' r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0)
      (leftStr ++ sepStr ++ rightStr, st'')
    | Layout.vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      let (topStr, st') := renderLayout top st r c topH w
      -- Draw horizontal separator
      let mut sepStr : Array String := #[]
      if h > topH then
        let sepRow := r + topH
        sepStr := sepStr.push (Terminal.moveCursorStr sepRow c)
        for _ in [0:w] do
           sepStr := sepStr.push st.config.hSplitStr
      let (bottomStr, st'') := renderLayout bottom st' (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w
      (topStr ++ sepStr ++ bottomStr, st'')
  let layoutH := rows - 1
  let (layoutStr, state) := renderLayout ws.layout state 0 0 layoutH cols
  buffer := buffer ++ layoutStr
  -- Global Status / Command Line
  buffer := buffer.push (Terminal.moveCursorStr (rows - 1) 0)
  let statusRight :=
    if state.mode == .command then s!":{state.inputState.commandBuffer}"
    else if state.mode == .searchForward then s!"/{state.inputState.commandBuffer}"
    else if state.mode == .searchBackward then s!"?{state.inputState.commandBuffer}"
    else state.message
  buffer := buffer.push statusRight
  buffer := buffer.push Terminal.clearLineStr
  -- Set Physical Cursor
  let rec getCursorPos (l : Layout) (r c h w : Nat) : Option (Nat × Nat) :=
    match l with
    | Layout.window id view =>
      if id == ws.activeWindowId then
--         let buf := getBuffer state view.bufferId
         let workH := if h > 0 then h - 1 else 0
         let colOffset := if state.config.showLineNumbers then 4 else 0
         let visualRow := view.cursor.row.val - view.scrollRow.val
         if visualRow >= 0 && visualRow < workH then
--             let rIdx : Row := ⟨view.scrollRow.val + visualRow⟩
             if view.cursor.col.val < view.scrollCol.val then
               none
             else
               let visualCol := view.cursor.col.val - view.scrollCol.val
               if (visualCol + colOffset) < w then
                  some (r + visualRow, c + visualCol + colOffset)
               else none
         else none
      else none
    | Layout.hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      (getCursorPos left r c h leftW).orElse (fun _ => getCursorPos right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0))
    | Layout.vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      (getCursorPos top r c topH w).orElse (fun _ => getCursorPos bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w)
  buffer := buffer.push (
    match getCursorPos ws.layout 0 0 layoutH cols with
    | some (pr, pc) => Terminal.moveCursorStr pr pc
    | none => "" -- Cursor hidden or out of view
  )
  if state.mode == .command then
     buffer := buffer.push (Terminal.moveCursorStr (rows - 1) (1 + state.inputState.commandBuffer.length))
  if state.mode == .searchForward || state.mode == .searchBackward then
     buffer := buffer.push (Terminal.moveCursorStr (rows - 1) (1 + state.inputState.commandBuffer.length))
  if state.mode == .visual || state.mode == .visualBlock then
    buffer := buffer.push Terminal.hideCursorStr
  else
    buffer := buffer.push Terminal.showCursorStr
  -- Output everything
  let finalStr := String.intercalate "" buffer.toList
  IO.print finalStr
  (← IO.getStdout).flush
  return state
end ViE.UI

import ViE.UI.Primitives
import ViE.UI.Search
import ViE.UI.Overlay
import ViE.UI.Window
import ViE.UI.Render

import ViE.UI.Primitives
import ViE.UI.Search
import ViE.Terminal
namespace ViE.UI
open ViE
def renderWindow (state : EditorState) (windowId : Nat) (view : ViewState) (rect : Rect) : (Array String × EditorState) := Id.run do
  let r := rect.row
  let c := rect.col
  let h := rect.height
  let w := rect.width
  let workH := if h > 0 then h - 1 else 0
  let buf0 := getWorkspaceBuffer state view.bufferId
  let mut currentSt := state
  let mut winBuf : Array String := #[]
  let prefetchMargin := 20
  let totalLines := FileBuffer.lineCount buf0
  let startRow := if view.scrollRow.val > prefetchMargin then view.scrollRow.val - prefetchMargin else 0
  let endRow := min totalLines (view.scrollRow.val + workH + prefetchMargin)
  currentSt := prefetchSearchLineMatches currentSt buf0 startRow endRow
  for i in [0:workH] do
    let lineIdx : Row := ⟨view.scrollRow.val + i⟩
    let screenRow := r + i
    winBuf := winBuf.push (Terminal.moveCursorStr screenRow c)
    let buf := getWorkspaceBuffer currentSt view.bufferId
    if lineIdx.val < FileBuffer.lineCount buf then
      let lnWidth := if state.config.showLineNumbers then 4 else 0
      let availableWidth := if w > lnWidth then w - lnWidth else 0
      let cachedLine := buf.cache.find lineIdx
      let cachedRaw := buf.cache.findRaw lineIdx
      let cachedIdx := buf.cache.findIndex lineIdx
      let lineStr := cachedRaw.getD (getLineFromBuffer buf lineIdx |>.getD "")
      let lineIndex := cachedIdx.getD (ViE.Unicode.buildDisplayByteIndex lineStr)
      let (displayLine, nextSt) :=
        match cachedLine with
        | some (s, cachedScrollCol, cachedWidth) =>
            if cachedScrollCol == view.scrollCol.val && cachedWidth == availableWidth then
              (s, currentSt)
            else
              match getLineFromBuffer buf lineIdx with
              | some lineStr =>
                  let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val
                  let dl := takeVisual sub availableWidth
                  let cache := match cachedRaw, cachedIdx with
                    | some raw, some _ =>
                        if raw == lineStr then
                          buf.cache
                        else
                          (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                    | _, _ =>
                        (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                  let cache := (cache.update lineIdx dl view.scrollCol.val availableWidth).updateRaw lineIdx lineStr
                  let updatedBuf := { buf with cache := cache }
                  let s' := currentSt.updateCurrentWorkspace fun ws =>
                    { ws with buffers := ws.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
                  (dl, s')
              | none => ("", currentSt)
        | none =>
            if let some lineStr := getLineFromBuffer buf lineIdx then
              let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.val
              let dl := takeVisual sub availableWidth
              let cache := match cachedRaw, cachedIdx with
                | some raw, some _ =>
                    if raw == lineStr then
                      buf.cache
                    else
                      (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
                | _, _ =>
                    (buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))
              let cache := (cache.update lineIdx dl view.scrollCol.val availableWidth).updateRaw lineIdx lineStr
              let updatedBuf := { buf with cache := cache }
              let s' := currentSt.updateCurrentWorkspace fun ws =>
                { ws with buffers := ws.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
              (dl, s')
            else
              ("", currentSt)
      currentSt := nextSt
      if state.config.showLineNumbers then
        winBuf := winBuf.push s!"{leftPad (toString (lineIdx.val + 1)) 3} "
      let isVisual := state.mode == Mode.visual || state.mode == Mode.visualBlock
      let selRange := if isVisual then state.selectionStart else none
      let (searchMatches, searchSt) := getLineSearchMatches currentSt buf.id lineIdx lineStr
      currentSt := searchSt
      let needsStyled := selRange.isSome || !searchMatches.isEmpty
      if !needsStyled then
        winBuf := winBuf.push displayLine
      else
        let mut styleActive := false
        let chars := displayLine.toList
        let mut dispIdx := 0
        let cursorByte :=
          if lineIdx == view.cursor.row then
            some (ViE.Unicode.displayColToByteOffsetFromIndex lineIndex view.cursor.col.val)
          else
            none
        let activeMatch := activeMatchRange searchMatches cursorByte
        for ch in chars do
          let chW := Unicode.charWidth ch
          let colVal := view.scrollCol.val + dispIdx
          let byteStart := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex colVal
          let byteEnd := ViE.Unicode.displayColToByteOffsetFromIndex lineIndex (colVal + chW)
          let isSelected :=
            state.isInSelection lineIdx ⟨colVal⟩ ||
            (chW > 1 && state.isInSelection lineIdx ⟨colVal + 1⟩)
          let isMatched :=
            searchMatches.any (fun m => overlapsByteRange m byteStart byteEnd)
          let isActiveMatched :=
            match activeMatch with
            | some m => overlapsByteRange m byteStart byteEnd
            | none => false
          if isSelected then
            if !styleActive then
              winBuf := winBuf.push "\x1b[7m"
              styleActive := true
          else if isMatched then
            if !styleActive then
              if isActiveMatched then
                winBuf := winBuf.push state.config.searchHighlightCursorStyle
              else
                winBuf := winBuf.push state.config.searchHighlightStyle
              styleActive := true
          else if styleActive then
            winBuf := winBuf.push "\x1b[0m"
            styleActive := false
          winBuf := winBuf.push ch.toString
          dispIdx := dispIdx + chW
        if styleActive then
          winBuf := winBuf.push "\x1b[0m"
    else
      winBuf := winBuf.push state.config.emptyLineMarker
    winBuf := winBuf.push Terminal.clearLineStr
  let statusRow := r + workH
  let statusBuf := getWorkspaceBuffer currentSt view.bufferId
  winBuf := winBuf.push (Terminal.moveCursorStr statusRow c)
  let fileName := statusBuf.filename.getD "[No Name]"
  let modeStr := if windowId == currentSt.getCurrentWorkspace.activeWindowId then s!"-- {state.mode} --" else "--"
  let eolMark := if statusBuf.missingEol then " [noeol]" else ""
  let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{windowId} B:{view.bufferId}] [{state.getCurrentWorkgroup.name}] {state.getCurrentWorkspace.name}"
  winBuf := winBuf.push state.config.statusBarStyle
  winBuf := winBuf.push statusStr.trimAscii.toString
  winBuf := winBuf.push Terminal.clearLineStr
  winBuf := winBuf.push state.config.resetStyle
  (winBuf, currentSt)
def renderFloatingWindow
    (st : EditorState)
    (view : ViewState)
    (rect : Rect)
    (borderFlags : FloatingWindowBorderFlags)
    : (Array String × Option (Nat × Nat)) := Id.run do
  let top := rect.row
  let left := rect.col
  let h := rect.height
  let w := rect.width
  let topBorderH := if borderFlags.top then 1 else 0
  let rightBorderW := if borderFlags.right then 1 else 0
  let bottomBorderH := if borderFlags.bottom then 1 else 0
  let leftBorderW := if borderFlags.left then 1 else 0
  let topBottomBorderH := topBorderH + bottomBorderH
  let sideBorderW := leftBorderW + rightBorderW
  if h < topBottomBorderH + 1 || w < sideBorderW + 1 then
    return (#[], none)
  let buf := getWorkspaceBuffer st view.bufferId
  let innerW := if w > sideBorderW then w - sideBorderW else 1
  let innerH := if h > topBottomBorderH then h - topBottomBorderH else 1
  let lnWidth := if st.config.showLineNumbers then 4 else 0
  let textW := if innerW > lnWidth then innerW - lnWidth else 1
  let repeatToken (token : String) (n : Nat) : String :=
    String.intercalate "" (List.replicate n token)
  let hBorder := if st.config.hSplitStr.isEmpty then "-" else st.config.hSplitStr
  let vBorder := if st.config.vSplitStr.isEmpty then "|" else st.config.vSplitStr
  let leftBorder := if borderFlags.left then vBorder else ""
  let rightBorder := if borderFlags.right then vBorder else ""
  let border := repeatToken hBorder w
  let mut out : Array String := #[]
  out := out.push st.config.resetStyle
  if borderFlags.top then
    out := out.push (Terminal.moveCursorStr top left)
    out := out.push border
  let isVisual := st.mode == Mode.visual || st.mode == Mode.visualBlock
  let hasSelection := isVisual && st.selectionStart.isSome
  for i in [0:innerH] do
    let lineIdx : Row := ⟨view.scrollRow.val + i⟩
    let raw := if lineIdx.val < FileBuffer.lineCount buf then getLineFromBuffer buf lineIdx |>.getD "" else ""
    let sub := ViE.Unicode.dropByDisplayWidth raw.toRawSubstring view.scrollCol.val
    let plainShown := takeVisual sub textW
    let shownW := Unicode.stringWidth plainShown
    let shown :=
      if hasSelection then
        Id.run do
          let mut styled : Array String := #[]
          let mut styleActive := false
          let mut dispCol := view.scrollCol.val
          for ch in plainShown.toList do
            let chW := Unicode.charWidth ch
            let selected :=
              st.isInSelection lineIdx ⟨dispCol⟩ ||
              (chW > 1 && st.isInSelection lineIdx ⟨dispCol + 1⟩)
            if selected then
              if !styleActive then
                styled := styled.push "\x1b[7m"
                styleActive := true
            else if styleActive then
              styled := styled.push st.config.resetStyle
              styleActive := false
            styled := styled.push ch.toString
            dispCol := dispCol + chW
          if styleActive then
            styled := styled.push st.config.resetStyle
          return String.intercalate "" styled.toList
      else
        plainShown
    let padW := if shownW < textW then textW - shownW else 0
    let pad := "".pushn ' ' padW
    let withNo :=
      if st.config.showLineNumbers then
        s!"{leftPad (toString (lineIdx.val + 1)) 3} {shown}{pad}"
      else
        s!"{shown}{pad}"
    out := out.push (Terminal.moveCursorStr (top + topBorderH + i) left)
    out := out.push s!"{leftBorder}{withNo}{rightBorder}"
  if borderFlags.bottom then
    out := out.push (Terminal.moveCursorStr (top + h - 1) left)
    out := out.push border
  out := out.push st.config.resetStyle
  let cursorPos : Option (Nat × Nat) :=
    if view.cursor.row.val < view.scrollRow.val then
      none
    else
      let visRow := view.cursor.row.val - view.scrollRow.val
      if visRow < innerH then
        let visCol := if view.cursor.col.val >= view.scrollCol.val then view.cursor.col.val - view.scrollCol.val else 0
        let colOff := if st.config.showLineNumbers then 4 else 0
        let c := min (innerW - 1) (colOff + visCol)
        some (top + topBorderH + visRow, left + leftBorderW + c)
      else
        none
  return (out, cursorPos)
end ViE.UI

import ViE.UI.Primitives
namespace ViE.UI
open ViE
/-- 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 overlapsByteRange (r : Nat × Nat) (byteStart byteEnd : Nat) : Bool :=
  let (s, e) := r
  byteStart < e && byteEnd > s
def activeMatchRange (hitRanges : Array (Nat × Nat)) (cursorByte : Option Nat) : Option (Nat × Nat) :=
  match cursorByte with
  | none => none
  | some cb =>
      let rec loop (i : Nat) : Option (Nat × Nat) :=
        if i >= hitRanges.size then
          none
        else
          let m := hitRanges[i]!
          let (s, e) := m
          if s <= cb && cb < e then
            some m
          else
            loop (i + 1)
      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 } }
def ensureSearchLineCacheForBuffer (st : EditorState) (bufferId : Nat) : EditorState :=
  match st.searchState with
  | none => st
  | some ss =>
      if ss.lineCacheBufferId == some bufferId then
        st
      else
        {
          st with
            searchState := some {
              ss with
                lineCacheBufferId := some bufferId
                lineMatches := Lean.RBMap.empty
                lineOrder := #[]
            }
        }
def getLineSearchMatches
    (st : EditorState)
    (bufferId : Nat)
    (lineIdx : Row)
    (lineStr : String)
    : (Array (Nat × Nat) × EditorState) :=
  let st := ensureSearchLineCacheForBuffer st bufferId
  match st.searchState with
  | none => (#[], st)
  | some ss =>
      if ss.pattern.isEmpty then
        (#[], st)
      else
        match ss.lineMatches.find? lineIdx with
        | some (cachedLine, cachedMatches) =>
            if cachedLine == lineStr then
              (cachedMatches, st)
            else
              let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss.pattern.toUTF8
              let st' := updateSearchLineCache st lineIdx lineStr matchRanges
              (matchRanges, st')
        | none =>
            let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss.pattern.toUTF8
            let st' := updateSearchLineCache st lineIdx lineStr matchRanges
            (matchRanges, st')
def prefetchSearchLineMatches
    (st : EditorState)
    (buf : FileBuffer)
    (startRow endRow : Nat)
    : EditorState :=
  let rec loop (row : Nat) (acc : EditorState) : EditorState :=
    if row >= endRow then
      acc
    else if row >= FileBuffer.lineCount buf then
      acc
    else
      let lineIdx : Row := ⟨row⟩
      let lineStr := getLineFromBuffer buf lineIdx |>.getD ""
      let (_, acc') := getLineSearchMatches acc buf.id lineIdx lineStr
      loop (row + 1) acc'
  loop startRow st
end ViE.UI

import ViE.UI.Window
import ViE.UI.Overlay
import ViE.Terminal
namespace ViE.UI
open ViE
/-- Render the current editor state to the terminal. -/
def render (state : EditorState) : IO EditorState := do
  if !state.dirty then return state
  -- Start building the frame buffer
  let mut buffer : Array String := #[]
  buffer := buffer.push Terminal.hideCursorStr
  let (rows, cols) ← Terminal.getWindowSize
  let ws := state.getCurrentWorkspace
  let rec renderLayout (l : Layout) (st : EditorState) (r c h w : Nat) : (Array String × EditorState) := Id.run do
    match l with
    | Layout.window id view =>
      if st.getCurrentWorkspace.isFloatingWindow id then
        let mut blankBuf : Array String := #[]
        for i in [0:h] do
          blankBuf := blankBuf.push (Terminal.moveCursorStr (r + i) c)
          blankBuf := blankBuf.push ("".pushn ' ' w)
        return (blankBuf, st)
      renderWindow st id view { row := r, col := c, height := h, width := w }
    | Layout.hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      let (leftStr, st') := renderLayout left st r c h leftW
      -- Draw vertical separator
      let mut sepStr : Array String := #[]
      if w > leftW then
        let sepCol := c + leftW
        for i in [0:h] do
           sepStr := sepStr.push (Terminal.moveCursorStr (r + i) sepCol)
           sepStr := sepStr.push st.config.vSplitStr
      let (rightStr, st'') := renderLayout right st' r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0)
      (leftStr ++ sepStr ++ rightStr, st'')
    | Layout.vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      let (topStr, st') := renderLayout top st r c topH w
      -- Draw horizontal separator
      let mut sepStr : Array String := #[]
      if h > topH then
        let sepRow := r + topH
        sepStr := sepStr.push (Terminal.moveCursorStr sepRow c)
        for _ in [0:w] do
           sepStr := sepStr.push st.config.hSplitStr
      let (bottomStr, st'') := renderLayout bottom st' (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w
      (topStr ++ sepStr ++ bottomStr, st'')
  let layoutH := rows - 1
  let baseLayout :=
    ws.getFloatingWindowIds.foldl (fun acc wid =>
      match acc with
      | some l => l.remove wid
      | none => none) (some ws.layout)
  if baseLayout.isNone then
    buffer := buffer.push Terminal.clearScreenStr
  buffer := buffer.push Terminal.homeCursorStr
  let (layoutStr, stateAfterLayout) :=
    match baseLayout with
    | some l => renderLayout l state 0 0 layoutH cols
    | none => (#[], state)
  buffer := buffer ++ layoutStr
  let wsAfterLayout := stateAfterLayout.getCurrentWorkspace
  let floatingViews := wsAfterLayout.getFloatingWindowIds.foldl (fun acc wid =>
    match wsAfterLayout.layout.findView wid with
    | some v => acc.push (wid, v)
    | none => acc) #[]
  let mut activeFloatingCursorPos : Option (Nat × Nat) := none
  for i in [0:floatingViews.size] do
    let (wid, view) := floatingViews[i]!
    match stateAfterLayout.getFloatingWindowBounds wid with
    | some (top, left, h, w) =>
      let borderFlags := stateAfterLayout.getFloatingWindowBorderFlags wid
      let (winBuf, cursorPos) := renderFloatingWindow stateAfterLayout view { row := top, col := left, height := h, width := w } borderFlags
      buffer := buffer ++ winBuf
      if wid == wsAfterLayout.activeWindowId then
        activeFloatingCursorPos := cursorPos
    | none => pure ()
  -- Global Status / Command Line
  buffer := buffer.push (Terminal.moveCursorStr (rows - 1) 0)
  let statusRight := renderStatusBar stateAfterLayout
  buffer := buffer.push statusRight
  buffer := buffer.push Terminal.clearLineStr
  let overlayToRender := stateAfterLayout.floatingOverlay.orElse (fun _ => messageOverlayForState stateAfterLayout)
  if let some overlay := overlayToRender then
    buffer := buffer ++ renderFloatingOverlay rows cols overlay
  -- Set Physical Cursor
  let rec getCursorPos (l : Layout) (r c h w : Nat) : Option (Nat × Nat) :=
    match l with
    | Layout.window id view =>
      if id == wsAfterLayout.activeWindowId then
         let workH := if h > 0 then h - 1 else 0
         let colOffset := if stateAfterLayout.config.showLineNumbers then 4 else 0
         let visualRow := view.cursor.row.val - view.scrollRow.val
         if visualRow >= 0 && visualRow < workH then
             if view.cursor.col.val < view.scrollCol.val then
               none
             else
               let visualCol := view.cursor.col.val - view.scrollCol.val
               if (visualCol + colOffset) < w then
                  some (r + visualRow, c + visualCol + colOffset)
               else none
         else none
      else none
    | Layout.hsplit left right ratio =>
      let leftW := (Float.ofNat w * ratio).toUInt64.toNat
      (getCursorPos left r c h leftW).orElse (fun _ => getCursorPos right r (c + leftW + 1) h (if w > leftW then w - leftW - 1 else 0))
    | Layout.vsplit top bottom ratio =>
      let topH := (Float.ofNat h * ratio).toUInt64.toNat
      (getCursorPos top r c topH w).orElse (fun _ => getCursorPos bottom (r + topH + 1) c (if h > topH then h - topH - 1 else 0) w)
  let overlayCursorPos : Option (Nat × Nat) :=
    match stateAfterLayout.floatingOverlay with
    | none => none
    | some overlay =>
        match computeFloatingOverlayLayout rows cols overlay with
        | none => none
        | some layout =>
            let lines := if overlay.lines.isEmpty then #[""] else overlay.lines
            let maxRow := lines.size - 1
            let rowIdx := min overlay.cursorRow maxRow
            let line := lines[rowIdx]!
            let lineW := Unicode.stringWidth line
            let colIdx := min overlay.cursorCol lineW
            let visRow := min rowIdx (layout.contentRows - 1)
            let visCol := min colIdx layout.innerWidth
            some (layout.top + 1 + layout.titleRows + visRow, layout.left + 2 + visCol)
  if stateAfterLayout.floatingOverlay.isSome && stateAfterLayout.mode != .command &&
     stateAfterLayout.mode != .searchForward && stateAfterLayout.mode != .searchBackward then
    buffer := buffer.push (
      match overlayCursorPos with
      | some (pr, pc) => Terminal.moveCursorStr pr pc
      | none => ""
    )
  else if wsAfterLayout.isFloatingWindow wsAfterLayout.activeWindowId &&
      stateAfterLayout.mode != .command && stateAfterLayout.mode != .searchForward && stateAfterLayout.mode != .searchBackward then
    buffer := buffer.push (
      match activeFloatingCursorPos with
      | some (pr, pc) => Terminal.moveCursorStr pr pc
      | none => ""
    )
  else
    buffer := buffer.push (
      match getCursorPos (baseLayout.getD wsAfterLayout.layout) 0 0 layoutH cols with
      | some (pr, pc) => Terminal.moveCursorStr pr pc
      | none => ""
    )
  if stateAfterLayout.mode == .command then
     buffer := buffer.push (Terminal.moveCursorStr (rows - 1) (1 + stateAfterLayout.inputState.commandBuffer.length))
  if stateAfterLayout.mode == .searchForward || stateAfterLayout.mode == .searchBackward then
     buffer := buffer.push (Terminal.moveCursorStr (rows - 1) (1 + stateAfterLayout.inputState.commandBuffer.length))
  if stateAfterLayout.mode == .visual || stateAfterLayout.mode == .visualBlock then
    buffer := buffer.push Terminal.hideCursorStr
  else
    buffer := buffer.push Terminal.showCursorStr
  -- Output everything
  let finalStr := String.intercalate "" buffer.toList
  IO.print finalStr
  (← IO.getStdout).flush
  return stateAfterLayout
end ViE.UI

import ViE.State
import ViE.Unicode
namespace ViE.UI
open ViE
/-- Pad a string on the left with spaces until it reaches the given width. -/
def leftPad (s : String) (width : Nat) : String :=
  if s.length >= width then s
  else "".pushn ' ' (width - s.length) ++ s
/-- Take characters from substring until visual width limit is reached. -/
def takeVisual (s : Substring.Raw) (width : Nat) : String :=
  Unicode.takeByDisplayWidth s width
def rightPadVisual (s : String) (width : Nat) : String :=
  let w := Unicode.stringWidth s
  if w >= width then
    s
  else
    s ++ "".pushn ' ' (width - w)
structure Rect where
  row : Nat
  col : Nat
  height : Nat
  width : Nat
  deriving Inhabited
def getWorkspaceBuffer (st : EditorState) (id : Nat) : FileBuffer :=
  let ws := st.getCurrentWorkspace
  ws.buffers.find? (fun b => b.id == id) |>.getD initialFileBuffer
end ViE.UI

import ViE.UI.Primitives
import ViE.Terminal
import ViE.Color
namespace ViE.UI
open ViE
def shouldRenderMessageAsFloat (msg : String) : Bool :=
  let m := msg.trimAscii.toString
  if m.isEmpty then
    false
  else
    m.startsWith "Error" ||
    m.startsWith "Cannot" ||
    m.startsWith "Invalid" ||
    m.startsWith "Unknown" ||
    m.startsWith "No " ||
    m.startsWith "Empty " ||
    m.startsWith "Usage:" ||
    m.startsWith "failed" ||
    m.startsWith "Failed" ||
    m.contains "not found"
def renderStatusBar (state : EditorState) : String :=
  let plainMessage := state.message.trimAscii.toString
  let floatMessage := shouldRenderMessageAsFloat plainMessage
  if state.mode == .command then
    s!":{state.inputState.commandBuffer}"
  else if state.mode == .searchForward then
    s!"/{state.inputState.commandBuffer}"
  else if state.mode == .searchBackward then
    s!"?{state.inputState.commandBuffer}"
  else if floatMessage then
    ""
  else
    plainMessage
def messageOverlayForState (state : EditorState) : Option FloatingOverlay :=
  let plainMessage := state.message.trimAscii.toString
  let floatMessage := shouldRenderMessageAsFloat plainMessage
  if state.floatingOverlay.isNone &&
      state.mode != .command &&
      state.mode != .searchForward &&
      state.mode != .searchBackward &&
      floatMessage then
    if plainMessage.isEmpty then
      none
    else
      some {
        title := "Message"
        lines := (plainMessage.splitOn "\n").toArray
        maxWidth := 0
        cursorRow := 0
        cursorCol := 0
      }
  else
    none
structure FloatingOverlayLayout where
  top : Nat
  left : Nat
  innerWidth : Nat
  titleRows : Nat
  contentRows : Nat
  deriving Inhabited
def computeFloatingOverlayLayout (rows cols : Nat) (overlay : FloatingOverlay) : Option FloatingOverlayLayout := Id.run do
  let availableRows := if rows > 1 then rows - 1 else rows
  if cols < 8 || availableRows < 4 then
    return none
  let lines := if overlay.lines.isEmpty then #[""] else overlay.lines
  let titleText := if overlay.title.isEmpty then "" else s!"[{overlay.title}]"
  let titleRows := if titleText.isEmpty then 0 else 1
  let naturalWidthContent := lines.foldl (fun acc ln => max acc (Unicode.stringWidth ln)) 0
  let naturalWidth := max naturalWidthContent (Unicode.stringWidth titleText)
  let maxInnerWidth := if cols > 8 then cols - 8 else 1
  let targetWidth :=
    if overlay.maxWidth > 0 then
      overlay.maxWidth
    else
      naturalWidth
  let innerWidth := max 1 (min targetWidth maxInnerWidth)
  let maxContentRows :=
    if availableRows > titleRows + 2 then
      availableRows - titleRows - 2
    else
      0
  if maxContentRows == 0 then
    return none
  let naturalRows := lines.size
  let targetRows := naturalRows
  let contentRows := max 1 (min targetRows maxContentRows)
  let boxHeight := contentRows + titleRows + 2
  let boxWidth := innerWidth + 4
  let top := (availableRows - boxHeight) / 2
  let left := (cols - boxWidth) / 2
  return some {
    top := top
    left := left
    innerWidth := innerWidth
    titleRows := titleRows
    contentRows := contentRows
  }
def renderFloatingOverlay (rows cols : Nat) (overlay : FloatingOverlay) : Array String := Id.run do
  let some layout := computeFloatingOverlayLayout rows cols overlay | return #[]
  let lines := if overlay.lines.isEmpty then #[""] else overlay.lines
  let titleText := if overlay.title.isEmpty then "" else s!"[{overlay.title}]"
  let top := layout.top
  let left := layout.left
  let innerWidth := layout.innerWidth
  let titleRows := layout.titleRows
  let contentRows := layout.contentRows
  let border := "+" ++ "".pushn '-' (innerWidth + 2) ++ "+"
  let style := (ViE.Color.toBg .brightBlack) ++ (ViE.Color.toFg .white)
  let mut out : Array String := #[]
  out := out.push (Terminal.moveCursorStr top left)
  out := out.push style
  out := out.push border
  if titleRows == 1 then
    out := out.push (Terminal.moveCursorStr (top + 1) left)
    let clippedTitle := Unicode.takeByDisplayWidth titleText.toRawSubstring innerWidth
    out := out.push s!"| {rightPadVisual clippedTitle innerWidth} |"
  for i in [0:contentRows] do
    let raw := lines[i]?.getD ""
    let clipped := Unicode.takeByDisplayWidth raw.toRawSubstring innerWidth
    let row := top + 1 + titleRows + i
    out := out.push (Terminal.moveCursorStr row left)
    out := out.push s!"| {rightPadVisual clipped innerWidth} |"
  let bottom := top + contentRows + titleRows + 1
  out := out.push (Terminal.moveCursorStr bottom left)
  out := out.push border
  out := out.push ViE.Color.reset
  return out
end ViE.UI

  lineCacheBufferId : Option Nat := none

  | buffers

structure FloatingOverlay where
  title : String
  lines : Array String
  maxWidth : Nat := 0
  cursorRow : Nat := 0
  cursorCol : Nat := 0
  deriving Repr, Inhabited

  floatingWindows : List Nat := []
  floatingWindowOffsets : List (Nat × Int × Int) := []

  floatingOverlay : Option FloatingOverlay
  floatingInputCommand : Option String := none

/-- Clear entire screen. -/
def clearScreenStr : String := "\x1b[2J"

  let bufferId := s.getActiveBuffer.id

    lineCacheBufferId := some bufferId

      let bufferId := s.getActiveBuffer.id

          lineCacheBufferId := some bufferId

def Layout.findWindowIdByBufferId (l : Layout) (bufferId : Nat) : Option Nat :=
  match l with
  | .window wid v => if v.bufferId == bufferId then some wid else none
  | .hsplit left right _ => (left.findWindowIdByBufferId bufferId).orElse (fun _ => right.findWindowIdByBufferId bufferId)
  | .vsplit top bottom _ => (top.findWindowIdByBufferId bufferId).orElse (fun _ => bottom.findWindowIdByBufferId bufferId)
def Layout.containsWindow (l : Layout) (windowId : Nat) : Bool :=
  match l with
  | .window wid _ => wid == windowId
  | .hsplit left right _ => left.containsWindow windowId || right.containsWindow windowId
  | .vsplit top bottom _ => top.containsWindow windowId || bottom.containsWindow windowId

  s.updateCurrentWorkspace fun ws =>
    let view := ws.layout.findView ws.activeWindowId
    match view with
    | some v =>
      let newBuffers := ws.buffers.map fun b =>
        if b.id == v.bufferId then
          let updated := FileBuffer.recomputeMissingEol (f b)
          FileBuffer.clearCache updated
        else b
      { ws with buffers := newBuffers }
    | none => ws

  let ws := s.getCurrentWorkspace
  let view := ws.layout.findView ws.activeWindowId
  let s' :=
    s.updateCurrentWorkspace fun ws =>
      match view with
      | some v =>
        let newBuffers := ws.buffers.map fun b =>
          if b.id == v.bufferId then
            let updated := FileBuffer.recomputeMissingEol (f b)
            FileBuffer.clearCache updated
          else b
        { ws with buffers := newBuffers }
      | none => ws
  match view, s'.searchState with
  | some v, some ss =>
      {
        s' with
          searchState := some {
            ss with
              lineCacheBufferId := some v.bufferId
              lineMatches := Lean.RBMap.empty
              lineOrder := #[]
          }
      }
  | _, _ => s'

def WorkspaceState.isFloatingWindow (ws : WorkspaceState) (windowId : Nat) : Bool :=
  ws.floatingWindows.contains windowId
def WorkspaceState.setWindowFloating (ws : WorkspaceState) (windowId : Nat) (enabled : Bool) : WorkspaceState :=
  if enabled then
    if ws.floatingWindows.contains windowId then ws
    else { ws with floatingWindows := windowId :: ws.floatingWindows }
  else
    {
      ws with
        floatingWindows := ws.floatingWindows.filter (fun wid => wid != windowId)
        floatingWindowOffsets := ws.floatingWindowOffsets.filter (fun (wid, _, _) => wid != windowId)
    }
def WorkspaceState.toggleWindowFloating (ws : WorkspaceState) (windowId : Nat) : WorkspaceState :=
  ws.setWindowFloating windowId (!ws.isFloatingWindow windowId)
def WorkspaceState.pruneFloatingWindows (ws : WorkspaceState) : WorkspaceState :=
  let rec idsOf (l : Layout) : List Nat :=
    match l with
    | .window id _ => [id]
    | .hsplit left right _ => idsOf left ++ idsOf right
    | .vsplit top bottom _ => idsOf top ++ idsOf bottom
  let ids := idsOf ws.layout
  {
    ws with
      floatingWindows := ws.floatingWindows.filter (fun wid => ids.contains wid)
      floatingWindowOffsets := ws.floatingWindowOffsets.filter (fun (wid, _, _) => ids.contains wid)
  }
def WorkspaceState.getFloatingWindowIds (ws : WorkspaceState) : Array Nat :=
  ws.floatingWindows.foldl (fun acc wid =>
    match ws.layout.findView wid with
    | some _ => acc.push wid
    | none => acc) #[]
def WorkspaceState.floatingWindowIndex? (ws : WorkspaceState) (windowId : Nat) : Option Nat :=
  let ids := ws.getFloatingWindowIds
  let rec loop (i : Nat) : Option Nat :=
    if i >= ids.size then
      none
    else if ids[i]! == windowId then
      some i
    else
      loop (i + 1)
  loop 0
def WorkspaceState.getFloatingWindowOffset (ws : WorkspaceState) (windowId : Nat) : Int × Int :=
  match ws.floatingWindowOffsets.find? (fun (wid, _, _) => wid == windowId) with
  | some (_, rowOff, colOff) => (rowOff, colOff)
  | none => (0, 0)
def WorkspaceState.setFloatingWindowOffset (ws : WorkspaceState) (windowId : Nat) (rowOff colOff : Int) : WorkspaceState :=
  let rest := ws.floatingWindowOffsets.filter (fun (wid, _, _) => wid != windowId)
  { ws with floatingWindowOffsets := (windowId, rowOff, colOff) :: rest }
def WorkspaceState.adjustFloatingWindowOffset (ws : WorkspaceState) (windowId : Nat) (dRow dCol : Int) : WorkspaceState :=
  let (rowOff, colOff) := ws.getFloatingWindowOffset windowId
  ws.setFloatingWindowOffset windowId (rowOff + dRow) (colOff + dCol)
structure FloatingWindowBorderFlags where
  top : Bool := true
  right : Bool := true
  bottom : Bool := true
  left : Bool := true
  deriving Inhabited
def WorkspaceState.layoutAllFloating (ws : WorkspaceState) (l : Layout) : Bool :=
  match l with
  | .window id _ => ws.isFloatingWindow id
  | .hsplit left right _ => ws.layoutAllFloating left && ws.layoutAllFloating right
  | .vsplit top bottom _ => ws.layoutAllFloating top && ws.layoutAllFloating bottom

def WorkspaceState.findFloatingSubtree (ws : WorkspaceState) (windowId : Nat) : Option Layout :=
  let rec go (l : Layout) : Option Layout :=
    if !l.containsWindow windowId then
      none
    else if ws.layoutAllFloating l then
      -- Outermost subtree containing the target where all descendants are floating.
      some l
    else
      match l with
      | .hsplit left right _ => (go left).orElse (fun _ => go right)
      | .vsplit top bottom _ => (go top).orElse (fun _ => go bottom)
      | .window _ _ => none
  go ws.layout

def computeFloatingWindowBounds (rows cols idx : Nat) : Option (Nat × Nat × Nat × Nat) :=
  let availableRows := if rows > 1 then rows - 1 else rows
  if availableRows < 6 || cols < 16 then
    none
  else
    let hMax := availableRows - 2
    let wMax := cols - 4
    let h := min hMax (max 8 ((availableRows * 3) / 5))
    let w := min wMax (max 24 ((cols * 3) / 5))
    let topBase := (availableRows - h) / 2
    let leftBase := (cols - w) / 2
    let top := min (availableRows - h) (topBase + idx)
    let left := min (cols - w) (leftBase + (2 * idx))
    some (top, left, h, w)
def EditorState.getFloatingWindowBounds (s : EditorState) (windowId : Nat) : Option (Nat × Nat × Nat × Nat) :=
  let ws := s.getCurrentWorkspace
  let floatingIds := ws.getFloatingWindowIds
  let rec indexOf (ids : Array Nat) (target : Nat) (i : Nat := 0) : Option Nat :=
    if i >= ids.size then none
    else if ids[i]! == target then some i
    else indexOf ids target (i + 1)
  let splitByRatio (total : Nat) (ratio : Float) : Option (Nat × Nat) :=
    if total < 2 then
      none
    else
      let raw := (Float.ofNat total * ratio).toUInt64.toNat
      let first := max 1 (min (total - 1) raw)
      some (first, total - first)
  let rec idsOfLayout (l : Layout) : List Nat :=
    match l with
    | .window id _ => [id]
    | .hsplit left right _ => idsOfLayout left ++ idsOfLayout right
    | .vsplit top bottom _ => idsOfLayout top ++ idsOfLayout bottom
  let minFloatingIndexOf (l : Layout) : Option Nat :=
    let ids := idsOfLayout l
    let rec loop (xs : List Nat) (best : Option Nat) : Option Nat :=
      match xs with
      | [] => best
      | id :: rest =>
        match indexOf floatingIds id, best with
        | some i, none => loop rest (some i)
        | some i, some b => loop rest (some (min i b))
        | none, _ => loop rest best
    loop ids none
  let rec locateInFloatingSubtree
      (l : Layout) (top left h w : Nat)
      : Option (Nat × Nat × Nat × Nat) :=
    match l with
    | .window id _ =>
      if id == windowId then some (top, left, h, w) else none
    | .hsplit leftL rightL ratio =>
      match splitByRatio w ratio with
      | none => none
      | some (leftW, rightW) =>
        (locateInFloatingSubtree leftL top left h leftW).orElse
          (fun _ => locateInFloatingSubtree rightL top (left + leftW) h rightW)
    | .vsplit topL bottomL ratio =>
      match splitByRatio h ratio with
      | none => none
      | some (topH, bottomH) =>
        (locateInFloatingSubtree topL top left topH w).orElse
          (fun _ => locateInFloatingSubtree bottomL (top + topH) left bottomH w)
  let floatingSubtreeBounds : Option (Nat × Nat × Nat × Nat) :=
    match ws.findFloatingSubtree windowId with
    | none => none
    | some subtree =>
      match minFloatingIndexOf subtree with
      | none => none
      | some groupIdx =>
        match computeFloatingWindowBounds s.windowHeight s.windowWidth groupIdx with
        | some (top, left, h, w) =>
          locateInFloatingSubtree subtree top left h w
        | none => none
  let baseBounds :=
    match floatingSubtreeBounds with
    | some b => some b
    | none =>
      match ws.floatingWindowIndex? windowId with
      | none => none
      | some idx => computeFloatingWindowBounds s.windowHeight s.windowWidth idx
  let toNatNonNeg (v : Int) : Nat :=
    if v < 0 then 0 else Int.toNat v
  let applyOffset (b : Nat × Nat × Nat × Nat) : Nat × Nat × Nat × Nat :=
    let (top, left, h, w) := b
    let (rowOff, colOff) := ws.getFloatingWindowOffset windowId
    let availableRows := if s.windowHeight > 1 then s.windowHeight - 1 else s.windowHeight
    let maxTop := if availableRows > h then availableRows - h else 0
    let maxLeft := if s.windowWidth > w then s.windowWidth - w else 0
    let rawTop := Int.ofNat top + rowOff
    let rawLeft := Int.ofNat left + colOff
    let top' := min maxTop (toNatNonNeg rawTop)
    let left' := min maxLeft (toNatNonNeg rawLeft)
    (top', left', h, w)
  baseBounds.map applyOffset
def EditorState.getFloatingWindowBorderFlags (s : EditorState) (windowId : Nat) : FloatingWindowBorderFlags :=
  let ws := s.getCurrentWorkspace
  let rec locateFlags
      (l : Layout)
      (acc : FloatingWindowBorderFlags)
      : Option FloatingWindowBorderFlags :=
    match l with
    | .window id _ =>
      if id == windowId then some acc else none
    | .hsplit left right _ =>
      let leftFlags := { acc with right := false }
      match locateFlags left leftFlags with
      | some f => some f
      | none =>
        let rightFlags := { acc with left := true }
        locateFlags right rightFlags
    | .vsplit top bottom _ =>
      let topFlags := { acc with bottom := false }
      match locateFlags top topFlags with
      | some f => some f
      | none =>
        let bottomFlags := { acc with top := true }
        locateFlags bottom bottomFlags
  match ws.findFloatingSubtree windowId with
  | some subtree =>
    (locateFlags subtree { top := true, right := true, bottom := true, left := true }).getD
      { top := true, right := true, bottom := true, left := true }
  | none => { top := true, right := true, bottom := true, left := true }

def EditorState.getActiveWindowScrollBounds (s : EditorState) : Nat × Nat :=
  let ws := s.getCurrentWorkspace
  let activeId := ws.activeWindowId
  if ws.isFloatingWindow activeId then
    match s.getFloatingWindowBounds activeId with
    | some (_, _, h, w) =>
      -- Floating window has a border, so scrollable area is smaller than outer bounds.
      let borderFlags := s.getFloatingWindowBorderFlags activeId
      let topBottomBorders := (if borderFlags.top then 1 else 0) + (if borderFlags.bottom then 1 else 0)
      let contentRows := if h > topBottomBorders then h - topBottomBorders else 1
      let h' := contentRows + 1
      let sideBorders := (if borderFlags.left then 1 else 0) + (if borderFlags.right then 1 else 0)
      let w' := if w > sideBorders then w - sideBorders else 1
      (h', w')
    | none =>
      s.getActiveWindowBounds
  else
    s.getActiveWindowBounds

  floatingOverlay := none
  floatingInputCommand := none

def arrayInsertAt (arr : Array α) (idx : Nat) (x : α) : Array α :=
  let i := min idx arr.size
  (arr.toList.take i ++ [x] ++ arr.toList.drop i).toArray
def arrayEraseAt (arr : Array α) (idx : Nat) : Array α :=
  if idx >= arr.size then arr
  else
    (arr.toList.take idx ++ arr.toList.drop (idx + 1)).toArray
def overlayLineLen (line : String) : Nat :=
  line.toList.length
def overlayNormalize (ov : FloatingOverlay) : FloatingOverlay :=
  if ov.lines.isEmpty then
    { ov with lines := #[""], cursorRow := 0, cursorCol := 0 }
  else
    let row := min ov.cursorRow (ov.lines.size - 1)
    let col := min ov.cursorCol (overlayLineLen (ov.lines[row]!))
    { ov with cursorRow := row, cursorCol := col }
def updateOverlay (s : EditorState) (f : FloatingOverlay → FloatingOverlay) : EditorState :=
  match s.floatingOverlay with
  | none => s
  | some ov =>
      { s with
          floatingOverlay := some (overlayNormalize (f ov))
          dirty := true
      }
def overlayMoveLeft (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    if ov.cursorCol > 0 then { ov with cursorCol := ov.cursorCol - 1 } else ov)
def overlayMoveRight (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    let len := overlayLineLen (ov.lines[ov.cursorRow]!)
    if ov.cursorCol < len then { ov with cursorCol := ov.cursorCol + 1 } else ov)
def overlayMoveUp (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    if ov.cursorRow > 0 then { ov with cursorRow := ov.cursorRow - 1 } else ov)
def overlayMoveDown (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    if ov.cursorRow + 1 < ov.lines.size then { ov with cursorRow := ov.cursorRow + 1 } else ov)
def overlayMoveLineStart (s : EditorState) : EditorState :=
  updateOverlay s (fun ov => { ov with cursorCol := 0 })
def overlayMoveLineEnd (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    { ov with cursorCol := overlayLineLen (ov.lines[ov.cursorRow]!) })
def overlayInsertChar (s : EditorState) (c : Char) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    let row := ov.cursorRow
    let col := ov.cursorCol
    let line := ov.lines[row]!
    let chars := line.toList
    let newLine := String.ofList (chars.take col ++ [c] ++ chars.drop col)
    { ov with lines := ov.lines.set! row newLine, cursorCol := col + 1 })
def overlayBackspace (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    let row := ov.cursorRow
    let col := ov.cursorCol
    let line := ov.lines[row]!
    if col > 0 then
      let chars := line.toList
      let newLine := String.ofList (chars.take (col - 1) ++ chars.drop col)
      { ov with lines := ov.lines.set! row newLine, cursorCol := col - 1 }
    else if row > 0 then
      let prev := ov.lines[row - 1]!
      let merged := prev ++ line
      let lines := (ov.lines.set! (row - 1) merged)
      let lines := arrayEraseAt lines row
      { ov with lines := lines, cursorRow := row - 1, cursorCol := overlayLineLen prev }
    else
      ov)
def overlayDeleteCharAt (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    let row := ov.cursorRow
    let col := ov.cursorCol
    let line := ov.lines[row]!
    let len := overlayLineLen line
    if col < len then
      let chars := line.toList
      let newLine := String.ofList (chars.take col ++ chars.drop (col + 1))
      { ov with lines := ov.lines.set! row newLine }
    else if row + 1 < ov.lines.size then
      let next := ov.lines[row + 1]!
      let merged := line ++ next
      let lines := (ov.lines.set! row merged)
      let lines := arrayEraseAt lines (row + 1)
      { ov with lines := lines }
    else
      ov)
def overlayInsertNewline (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    let row := ov.cursorRow
    let col := ov.cursorCol
    let line := ov.lines[row]!
    let chars := line.toList
    let left := String.ofList (chars.take col)
    let right := String.ofList (chars.drop col)
    let lines := (ov.lines.set! row left)
    let lines := arrayInsertAt lines (row + 1) right
    { ov with lines := lines, cursorRow := row + 1, cursorCol := 0 })
def overlayOpenLineBelow (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    let row := ov.cursorRow + 1
    let lines := arrayInsertAt ov.lines row ""
    { ov with lines := lines, cursorRow := row, cursorCol := 0 })
def overlayOpenLineAbove (s : EditorState) : EditorState :=
  updateOverlay s (fun ov =>
    let ov := overlayNormalize ov
    let row := ov.cursorRow
    let lines := arrayInsertAt ov.lines row ""
    { ov with lines := lines, cursorRow := row, cursorCol := 0 })
def shouldRenderMessageAsFloat (msg : String) : Bool :=
  let m := msg.trimAscii.toString
  if m.isEmpty then
    false
  else
    m.startsWith "Error" ||
    m.startsWith "Cannot" ||
    m.startsWith "Invalid" ||
    m.startsWith "Unknown" ||
    m.startsWith "No " ||
    m.startsWith "Empty " ||
    m.startsWith "Usage:" ||
    m.startsWith "failed" ||
    m.startsWith "Failed" ||
    m.contains "not found"

  let submitFloatingInput (state : EditorState) : IO EditorState := do
    match state.floatingInputCommand, state.floatingOverlay with
    | some cmdPrefix, some ov =>
      let input := (ov.lines[0]?.getD "").trimAscii.toString
      let cmd := s!"{cmdPrefix}{input}"
      let pre := {
        state with
          floatingOverlay := none
          floatingInputCommand := none
          mode := .normal
          inputState := {
            state.inputState with
              commandBuffer := cmd
              countBuffer := ""
              previousKey := none
              pendingKeys := ""
          }
      }
      let out ← ViE.Command.executeCommand commands pre
      return {
        out with
          mode := .normal
          inputState := {
            out.inputState with
              commandBuffer := ""
              countBuffer := ""
              previousKey := none
              pendingKeys := ""
          }
          dirty := true
      }
    | _, _ =>
      return {
        state with
          floatingOverlay := none
          floatingInputCommand := none
          dirty := true
      }

  match k with
  | Key.char 'h' =>
      -- Check if in explorer buffer
      let buf := s.getActiveBuffer
      let isExplorer := s.explorers.any (fun (id, _) => id == buf.id)
      if isExplorer then
        -- Navigate to parent directory
        let explorerOpt := s.explorers.find? (fun (id, _) => id == buf.id)
        match explorerOpt with
        | some (_, explorer) =>
          let parentPath := match (System.FilePath.mk explorer.currentPath).parent with
            | some p => p.toString
            | none => "/"
          ViE.Feature.openExplorerWithPreview s parentPath explorer.previewWindowId explorer.previewBufferId
        | none => pure $ clearInput (EditorState.moveCursorLeftN s s.getCount)
      else

  let closeOverlay : EditorState :=
    { s with floatingOverlay := none, floatingInputCommand := none, dirty := true, message := "floating overlay cleared" }
  if s.floatingOverlay.isSome then
    if s.floatingInputCommand.isSome then
      match k with
      | Key.esc => pure { s with floatingOverlay := none, floatingInputCommand := none, mode := .normal, dirty := true, message := "" }
      | Key.enter => submitFloatingInput s
      | Key.char 'q' => pure { s with floatingOverlay := none, floatingInputCommand := none, mode := .normal, dirty := true, message := "" }
      | Key.left => pure (overlayMoveLeft s)
      | Key.right => pure (overlayMoveRight s)
      | Key.up => pure (overlayMoveUp s)
      | Key.down => pure (overlayMoveDown s)
      | Key.backspace => pure (overlayBackspace s)
      | Key.char c => pure (overlayInsertChar s c)
      | _ => pure s
    else
      match k with
      | Key.esc => pure closeOverlay
      | Key.enter => pure closeOverlay
      | Key.char 'q' => pure closeOverlay
      | Key.char ':' => pure $ s.setMode Mode.command
      | Key.char 'i' => pure { s with mode := .insert, dirty := true }
      | Key.char 'a' => pure { (overlayMoveRight s) with mode := .insert }
      | Key.char 'h' => pure (overlayMoveLeft s)
      | Key.char 'j' => pure (overlayMoveDown s)
      | Key.char 'k' => pure (overlayMoveUp s)
      | Key.char 'l' => pure (overlayMoveRight s)
      | Key.char '0' => pure (overlayMoveLineStart s)
      | Key.char '$' => pure (overlayMoveLineEnd s)
      | Key.char 'x' => pure (overlayDeleteCharAt s)
      | Key.char 'o' => pure { (overlayOpenLineBelow s) with mode := .insert }
      | Key.char 'O' => pure { (overlayOpenLineAbove s) with mode := .insert }
      | _ => pure s
  else
    if shouldRenderMessageAsFloat s.message then
      match k with
      | Key.esc => pure { s with message := "", dirty := true }
      | Key.enter => pure { s with message := "", dirty := true }
      | _ => pure s
    else
    match k with
    | Key.esc =>
        pure { s with inputState := { s.inputState with countBuffer := "", previousKey := none } }
    | Key.char 'h' =>
        -- Check if in explorer buffer
        let buf := s.getActiveBuffer
        let isExplorer := s.explorers.any (fun (id, _) => id == buf.id)
        if isExplorer then
          let explorerOpt := s.explorers.find? (fun (id, _) => id == buf.id)
          match explorerOpt with
          | some (_, explorer) =>
            if explorer.mode == .files then
              let parentPath := match (System.FilePath.mk explorer.currentPath).parent with
                | some p => p.toString
                | none => "/"
              ViE.Feature.openExplorerWithPreview s parentPath explorer.previewWindowId explorer.previewBufferId
            else
              handleMotion s EditorState.moveCursorLeft
          | none => pure $ clearInput (EditorState.moveCursorLeftN s s.getCount)
        else

        handleMotion s EditorState.moveCursorLeft
  | Key.char 'j' => do

          handleMotion s EditorState.moveCursorLeft
    | Key.char 'j' => do

  | Key.char 'k' => do

    | Key.char 'k' => do

  | Key.char 'l' => handleMotion s EditorState.moveCursorRight
  | Key.enter => ViE.Feature.handleExplorerEnter s
  | Key.char 'i' => pure $ s.setMode Mode.insert
  | Key.char 'a' =>

    | Key.char 'l' => handleMotion s EditorState.moveCursorRight
    | Key.enter => ViE.Feature.handleExplorerEnter s
    | Key.char 'i' => pure $ s.setMode Mode.insert
    | Key.char 'a' =>

  | Key.char 'A' =>

    | Key.char 'A' =>

  | Key.char ':' => pure $ s.setMode Mode.command
  | Key.char '/' =>

    | Key.char ':' => pure $ s.setMode Mode.command
    | Key.char '/' =>

  | Key.char '?' =>

    | Key.char '?' =>

  | Key.char 'q' => pure $ s.setMode Mode.command
  | Key.char 'o' => pure $ (EditorState.insertLineBelow s).setMode Mode.insert
  | Key.char 'O' => pure $ (EditorState.insertLineAbove s).setMode Mode.insert
  | Key.char 'v' => pure $ EditorState.startVisualMode s
  | Key.char 'V' => pure $ EditorState.startVisualBlockMode s
  | Key.char '0' =>

    | Key.char 'q' => pure $ s.setMode Mode.command
    | Key.char 'o' => pure $ (EditorState.insertLineBelow s).setMode Mode.insert
    | Key.char 'O' => pure $ (EditorState.insertLineAbove s).setMode Mode.insert
    | Key.char 'v' => pure $ EditorState.startVisualMode s
    | Key.char 'V' => pure $ EditorState.startVisualBlockMode s
    | Key.char '0' =>

  | Key.char '$' => handleMotion s EditorState.moveToLineEnd

    | Key.char '$' => handleMotion s EditorState.moveToLineEnd

  | Key.char 'w' =>

    | Key.char 'w' =>

  | Key.char 'b' => handleMotion s EditorState.moveWordBackward
  | Key.char 'e' => handleMotion s EditorState.moveWordEnd
  | Key.char 'x' => pure $ clearInput (EditorState.deleteCharAfterCursor s)
  | Key.char 'n' => pure $ clearInput (ViE.findNextMatch s)
  | Key.char 'N' =>

    | Key.char 'b' => handleMotion s EditorState.moveWordBackward
    | Key.char 'e' => handleMotion s EditorState.moveWordEnd
    | Key.char 'x' => pure $ clearInput (EditorState.deleteCharAfterCursor s)
    | Key.char 'n' => pure $ clearInput (ViE.findNextMatch s)
    | Key.char 'N' =>

  | Key.char 'p' =>

    | Key.char 'p' =>

  | Key.char 'P' => pure $ clearInput (EditorState.pasteAbove s)
  | Key.char 'y' =>

    | Key.char 'P' => pure $ clearInput (EditorState.pasteAbove s)
    | Key.char 'y' =>

  | Key.char '|' =>
    let n := s.getCount
    pure $ clearInput (EditorState.jumpToColumn s n)
  | Key.char 'c' =>
    match s.inputState.previousKey with
    | some 'c' =>
        -- cc: delete line and enter insert mode
        -- For now, approximate with delete line. Ideally should preserve line as empty.
        pure $ (s.deleteCurrentLine).setMode Mode.insert
    | _ => pure { s with inputState := { s.inputState with previousKey := some 'c' } }
  | Key.char 'd' =>
    match s.inputState.previousKey with
    | some 'd' => pure $ s.deleteCurrentLine
    | _ => pure { s with inputState := { s.inputState with previousKey := some 'd' } }
  | Key.char 'u' => pure $ s.undo
  | Key.ctrl 'r' => pure $ s.redo
  | Key.ctrl 'w' =>

    | Key.char '|' =>
      let n := s.getCount
      pure $ clearInput (EditorState.jumpToColumn s n)
    | Key.char 'c' =>
      match s.inputState.previousKey with
      | some 'c' =>
          -- cc: delete line and enter insert mode
          -- For now, approximate with delete line. Ideally should preserve line as empty.
          pure $ (s.deleteCurrentLine).setMode Mode.insert
      | _ => pure { s with inputState := { s.inputState with previousKey := some 'c' } }
    | Key.char 'd' =>
      match s.inputState.previousKey with
      | some 'd' => pure $ s.deleteCurrentLine
      | _ => pure { s with inputState := { s.inputState with previousKey := some 'd' } }
    | Key.char 'u' => pure $ s.undo
    | Key.ctrl 'r' => pure $ s.redo
    | Key.ctrl 'l' => pure { s with dirty := true, message := "redraw" }
    | Key.ctrl 'w' =>

  | Key.char c =>

    | Key.char c =>

  | Key.alt c =>

    | Key.alt c =>

      let activeIsFloating := s'.getCurrentWorkspace.isFloatingWindow s'.getCurrentWorkspace.activeWindowId

      | 'H' => pure $ resizeWindow s' .left 0.05
      | 'J' => pure $ resizeWindow s' .down 0.05
      | 'K' => pure $ resizeWindow s' .up 0.05
      | 'L' => pure $ resizeWindow s' .right 0.05

      | 'H' =>
        if activeIsFloating then
          pure $ nudgeActiveFloatingWindow s' .left
        else
          pure $ resizeWindow s' .left 0.05
      | 'J' =>
        if activeIsFloating then
          pure $ nudgeActiveFloatingWindow s' .down
        else
          pure $ resizeWindow s' .down 0.05
      | 'K' =>
        if activeIsFloating then
          pure $ nudgeActiveFloatingWindow s' .up
        else
          pure $ resizeWindow s' .up 0.05
      | 'L' =>
        if activeIsFloating then
          pure $ nudgeActiveFloatingWindow s' .right
        else
          pure $ resizeWindow s' .right 0.05

  | _ => pure { s with inputState := { s.inputState with countBuffer := "", previousKey := none } },

    | _ => pure { s with inputState := { s.inputState with countBuffer := "", previousKey := none } },

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

  insert := fun s k =>
    if s.floatingOverlay.isSome then
      if s.floatingInputCommand.isSome then
        let submitFloatingInput (state : EditorState) : IO EditorState := do
          match state.floatingInputCommand, state.floatingOverlay with
          | some cmdPrefix, some ov =>
            let input := (ov.lines[0]?.getD "").trimAscii.toString
            let cmd := s!"{cmdPrefix}{input}"
            let pre := {
              state with
                floatingOverlay := none
                floatingInputCommand := none
                mode := .normal
                inputState := {
                  state.inputState with
                    commandBuffer := cmd
                    countBuffer := ""
                    previousKey := none
                    pendingKeys := ""
                }
            }
            let out ← ViE.Command.executeCommand commands pre
            return {
              out with
                mode := .normal
                inputState := {
                  out.inputState with
                    commandBuffer := ""
                    countBuffer := ""
                    previousKey := none
                    pendingKeys := ""
                }
                dirty := true
            }
          | _, _ =>
            return {
              state with
                floatingOverlay := none
                floatingInputCommand := none
                mode := .normal
                dirty := true
            }
        match k with
        | Key.esc => pure { s with floatingOverlay := none, floatingInputCommand := none, mode := .normal, dirty := true, message := "" }
        | Key.backspace => pure (overlayBackspace s)
        | Key.char c => pure (overlayInsertChar s c)
        | Key.enter => submitFloatingInput s
        | Key.left => pure (overlayMoveLeft s)
        | Key.right => pure (overlayMoveRight s)
        | Key.up => pure (overlayMoveUp s)
        | Key.down => pure (overlayMoveDown s)
        | _ => pure s
      else
        match k with
        | Key.esc => pure { s with mode := .normal, dirty := true }
        | Key.backspace => pure (overlayBackspace s)
        | Key.char c => pure (overlayInsertChar s c)
        | Key.enter => pure (overlayInsertNewline s)
        | Key.left => pure (overlayMoveLeft s)
        | Key.right => pure (overlayMoveRight s)
        | Key.up => pure (overlayMoveUp s)
        | Key.down => pure (overlayMoveDown s)
        | _ => pure s
    else
      match k with
      | Key.esc => pure $ (s.commitEdit.moveCursorLeft).setMode Mode.normal
      | Key.backspace => pure $ s.deleteBeforeCursor
      | Key.char c => pure $ s.insertChar c
      | Key.enter => pure s.insertNewline
      | _ => pure s,

def flushEscSequence (seq : String) : List Key :=
  seq.toList.map (fun ch => if ch == '\x1b' then Key.esc else Key.char ch)
def isAsciiInRange (ch : Char) (lo hi : Nat) : Bool :=
  let n := ch.toNat
  lo <= n && n <= hi
def isCsiParamChar (ch : Char) : Bool :=
  ch.isDigit || ch == ';' || ch == '?' || ch == ':' || ch == '<' || ch == '=' || ch == '>'
def isCsiFinalChar (ch : Char) : Bool :=
  isAsciiInRange ch 0x40 0x7e
def decodeCsiFinal (ch : Char) : Key :=
  match ch with
  | 'A' => Key.up
  | 'B' => Key.down
  | 'C' => Key.right
  | 'D' => Key.left
  | 'H' => Key.unknown 'H'
  | 'F' => Key.unknown 'F'
  | _ => Key.unknown ch
def withPending (state : EditorState) (pending : String) (currentTime : Nat) : EditorState :=
  { state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }
def clearPending (state : EditorState) : EditorState :=
  { state with inputState := { state.inputState with pendingKeys := "" } }

  -- If we have pending keys (escape sequence in progress)

    -- Check for known sequences

      ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])

      (withPending state pending currentTime, [])

       -- CSI sequence starter, keep waiting
       ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
    | "\x1b[A" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.up])
    | "\x1b[B" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.down])
    | "\x1b[C" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.right])
    | "\x1b[D" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.left])
    | "\x1b[H" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'H']) -- Home?
    | "\x1b[F" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'F']) -- End?

      (withPending state pending currentTime, [])

       -- Treat ESC + <char> as Alt combination when it's a single character and not CSI.
       match pending.toList with
       | ['\x1b', ch] =>
         if ch != '[' then
           ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.alt ch])
         else
           ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
       | _ =>
       -- Unknown sequence or incomplete?
       -- If length is long enough (e.g. 3 chars) and no match, flush as individual keys?
       -- Or check if it starts with valid prefix.
       if pending.startsWith "\x1b[" && pending.length < 5 then
          ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
       else
          -- Flush everything as individual characters
          -- (Note: this simplifies, strictly we should map char-by-char)
          let keys := pending.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
          ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)

      match pending.toList with
      | ['\x1b', ch] =>
        if ch == '[' then
          (withPending state pending currentTime, [])
        else
          (clearPending state, [Key.alt ch])
      | _ =>
        if pending.startsWith "\x1b[" then
          let chars := pending.toList
          let last := chars.getLastD '\x00'
          if isCsiFinalChar last then
            (clearPending state, [decodeCsiFinal last])
          else if isCsiParamChar last && pending.length <= 12 then
            (withPending state pending currentTime, [])
          else if pending.length > 12 then
            (clearPending state, flushEscSequence pending)
          else
            (clearPending state, flushEscSequence pending)
        else
          (clearPending state, flushEscSequence pending)

    -- No pending keys

       -- Start escape sequence
       ({ state with inputState := { state.inputState with pendingKeys := "\x1b", lastInputTime := currentTime } }, [])

       (withPending state "\x1b" currentTime, [])

       -- Normal character (using logic similar to old fromChar)

    if currentTime - state.inputState.lastInputTime > 50 then -- 50ms timeout
       -- Timeout! Flush pending keys as is.
       let keys := state.inputState.pendingKeys.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
       ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)

    if currentTime - state.inputState.lastInputTime > 50 then
       let keys := flushEscSequence state.inputState.pendingKeys
       (clearPending state, keys)

import ViE.Key.Input

  -- If we have pending keys (escape sequence in progress)
  if state.inputState.pendingKeys.length > 0 then
    let pending := state.inputState.pendingKeys.push c
    -- Check for known sequences
    match pending with
    | "\x1b" =>
       ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
    | "\x1b[" =>
       -- CSI sequence starter, keep waiting
       ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
    | "\x1b[A" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.up])
    | "\x1b[B" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.down])
    | "\x1b[C" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.right])
    | "\x1b[D" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.left])
    | "\x1b[H" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'H']) -- Home?
    | "\x1b[F" => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.unknown 'F']) -- End?
    | _ =>
       -- Check for Alt+Char: Escape followed by a single char
       if pending.length == 2 && pending.startsWith "\x1b" then
          match pending.toList with
          | [_, c] => ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.alt c])
          | _ => -- Should be impossible given length check
             let keys := pending.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
             ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
       -- Check if it looks like a CSI sequence
       else if pending.startsWith "\x1b[" && pending.length < 5 then
          ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
       else
          -- Flush everything as individual characters
          let keys := pending.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
          ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
  else
    -- No pending keys
    if c == '\x1b' then
       -- Start escape sequence
       ({ state with inputState := { state.inputState with pendingKeys := "\x1b", lastInputTime := currentTime } }, [])
    else
       -- Normal character (using logic similar to old fromChar)
       let k := match c with
        | '\x01' => Key.ctrl 'a'
        | '\x02' => Key.ctrl 'b'
        | '\x03' => Key.ctrl 'c'
        | '\x04' => Key.ctrl 'd'
        | '\x05' => Key.ctrl 'e'
        | '\x06' => Key.ctrl 'f'
        | '\x07' => Key.ctrl 'g'
        | '\x08' => Key.ctrl 'h'
        | '\x09' => Key.ctrl 'i'
        | '\x0b' => Key.ctrl 'k'
        | '\x0c' => Key.ctrl 'l'
        | '\x0e' => Key.ctrl 'n'
        | '\x0f' => Key.ctrl 'o'
        | '\x10' => Key.ctrl 'p'
        | '\x11' => Key.ctrl 'q'
        | '\x12' => Key.ctrl 'r'
        | '\x13' => Key.ctrl 's'
        | '\x14' => Key.ctrl 't'
        | '\x15' => Key.ctrl 'u'
        | '\x16' => Key.ctrl 'v'
        | '\x17' => Key.ctrl 'w'
        | '\x18' => Key.ctrl 'x'
        | '\x19' => Key.ctrl 'y'
        | '\x1a' => Key.ctrl 'z'
        | '\x7f' => Key.backspace
        | '\x0a' | '\x0d' => Key.enter
        | _ => Key.char c
       (state, [k])

  ViE.Key.parseKey state c currentTime

  if state.inputState.pendingKeys.length > 0 then
    if currentTime - state.inputState.lastInputTime > 50 then -- 50ms timeout
       -- Timeout! Flush pending keys as is.
       let keys := state.inputState.pendingKeys.toList.map (fun x => if x == '\x1b' then Key.esc else Key.char x)
       ({ state with inputState := { state.inputState with pendingKeys := "" } }, keys)
    else
       (state, [])
  else
    (state, [])

  ViE.Key.checkTimeout state currentTime

  let (h, w) := state.getActiveWindowBounds

  let (h, w) := state.getActiveWindowScrollBounds

def cmdRedraw (_ : List String) (state : EditorState) : IO EditorState :=
  let s1 := state.updateCurrentWorkspace fun ws =>
    { ws with buffers := ws.buffers.map FileBuffer.clearCache }
  let s2 :=
    match s1.searchState with
    | some ss =>
        { s1 with
            searchState := some {
              ss with
                lineMatches := Lean.RBMap.empty
                lineOrder := #[]
            }
        }
    | none => s1
  return { s2 with dirty := true, message := "redraw" }
def floatUsage : String :=
  "Usage: :float [--title <title>|--title=<title>] [--width <cols>|--width=<cols>] <text> | :float clear"
def parsePositiveNat (s : String) : Option Nat :=
  match s.toNat? with
  | some n => if n > 0 then some n else none
  | none => none
partial def parseFloatArgs
  (args : List String)
  (title : String)
  (maxWidth : Nat)
  (textRev : List String)
  : Except String (String × Nat × List String) :=
  match args with
  | [] =>
      .ok (title, maxWidth, textRev.reverse)
  | "--" :: rest =>
      .ok (title, maxWidth, textRev.reverse ++ rest)
  | "--title" :: t :: rest =>
      parseFloatArgs rest t maxWidth textRev
  | "--title" :: [] =>
      .error floatUsage
  | "--width" :: w :: rest =>
      match parsePositiveNat w with
      | some n => parseFloatArgs rest title n textRev
      | none => .error s!"Invalid float width: {w}"
  | "--width" :: [] =>
      .error floatUsage
  | tok :: rest =>
      if tok.startsWith "--title=" then
        parseFloatArgs rest (tok.drop 8 |>.toString) maxWidth textRev
      else if tok.startsWith "--width=" then
        let w := (tok.drop 8).toString
        match parsePositiveNat w with
        | some n => parseFloatArgs rest title n textRev
        | none => .error s!"Invalid float width: {w}"
      else
        parseFloatArgs rest title maxWidth (tok :: textRev)
def cmdFloat (args : List String) (state : EditorState) : IO EditorState := do
  if args == ["clear"] then
    return { state with floatingOverlay := none, floatingInputCommand := none, dirty := true, message := "floating overlay cleared" }
  match parseFloatArgs args "Float" 0 [] with
  | .error msg =>
      return { state with message := msg }
  | .ok (titleRaw, maxWidth, textTokens) =>
      let raw := (String.intercalate " " textTokens).trimAscii.toString
      if raw.isEmpty then
        return { state with message := floatUsage }
      else
        let title := titleRaw.trimAscii.toString
        let lines := (raw.splitOn "\\n").toArray
        let lines := if lines.isEmpty then #[""] else lines
        let lastRow := lines.size - 1
        let lastCol := (lines[lastRow]!.toList.length)
        let overlay : FloatingOverlay := {
          title := if title.isEmpty then "Float" else title
          lines := lines
          maxWidth := maxWidth
          cursorRow := lastRow
          cursorCol := lastCol
        }
        return { state with floatingOverlay := some overlay, floatingInputCommand := none, dirty := true, message := "floating overlay shown" }
def cmdNoFloat (_ : List String) (state : EditorState) : IO EditorState :=
  return { state with floatingOverlay := none, floatingInputCommand := none, dirty := true, message := "floating overlay cleared" }
def cmdFloatWin (args : List String) (state : EditorState) : IO EditorState := do
  let usage := "Usage: :floatwin [toggle|on|off|clear]"
  let activeId := state.getCurrentWorkspace.activeWindowId
  let s' := state.updateCurrentWorkspace fun ws =>
    let ws := ws.pruneFloatingWindows
    match args with
    | [] => ws.toggleWindowFloating activeId
    | ["toggle"] => ws.toggleWindowFloating activeId
    | ["on"] => ws.setWindowFloating activeId true
    | ["off"] => ws.setWindowFloating activeId false
    | ["clear"] => { ws with floatingWindows := [], floatingWindowOffsets := [] }
    | _ => ws
  let ws' := s'.getCurrentWorkspace
  let isFloating := ws'.isFloatingWindow activeId
  let msg :=
    match args with
    | _ :: _ =>
        if args == ["clear"] then "floating windows cleared"
        else if args == ["on"] then s!"window {activeId} floating on"
        else if args == ["off"] then s!"window {activeId} floating off"
        else if args == ["toggle"] then
          if isFloating then s!"window {activeId} floating on" else s!"window {activeId} floating off"
        else usage
    | [] =>
        if isFloating then s!"window {activeId} floating on" else s!"window {activeId} floating off"
  return { s' with dirty := true, message := msg }

    let name := s!"Group {state.workgroups.size}"
    let nextBufId := state.workgroups.foldl (fun m g =>
      g.workspaces.foldl (fun m2 ws => max m2 ws.nextBufferId) m) 0
    let newWg := createEmptyWorkgroup name nextBufId
    let newState := { state with
      workgroups := state.workgroups.push newWg,
      currentGroup := state.workgroups.size -- switch to new one using the size before push
    }
    return { newState with message := s!"Created workgroup: {name}" }

    if state.mode == .command then
      return ViE.Feature.openNameInputFloat state "New Workgroup" "" "wg new "
    else
      let name := s!"Group {state.workgroups.size}"
      let nextBufId := state.workgroups.foldl (fun m g =>
        g.workspaces.foldl (fun m2 ws => max m2 ws.nextBufferId) m) 0
      let newWg := createEmptyWorkgroup name nextBufId
      let newState := { state with
        workgroups := state.workgroups.push newWg,
        currentGroup := state.workgroups.size -- switch to new one using the size before push
      }
      return { newState with message := s!"Created workgroup: {name}" }

    let nextBufId := state.workgroups.foldl (fun m g =>
      g.workspaces.foldl (fun m2 ws => max m2 ws.nextBufferId) m) 0
    let newWg := createEmptyWorkgroup name nextBufId
    let newState := { state with
      workgroups := state.workgroups.push newWg,
      currentGroup := state.workgroups.size
    }
    return { newState with message := s!"Created workgroup: {name}" }

    let trimmed := name.trimAscii.toString
    if trimmed.isEmpty then
      return { state with message := "Workgroup name cannot be empty" }
    else
      let nextBufId := state.workgroups.foldl (fun m g =>
        g.workspaces.foldl (fun m2 ws => max m2 ws.nextBufferId) m) 0
      let newWg := createEmptyWorkgroup trimmed nextBufId
      let newState := { state with
        workgroups := state.workgroups.push newWg,
        currentGroup := state.workgroups.size
      }
      return { newState with message := s!"Created workgroup: {trimmed}" }

    let name := s!"Workspace {wg.workspaces.size}"
    let newWs := makeWorkspaceState name none maxBufId
    let newState := state.updateCurrentWorkgroup fun wg =>
      { wg with
        workspaces := wg.workspaces.push newWs,
        currentWorkspace := wg.workspaces.size
      }
    return { newState with message := s!"Created workspace: {name}" }

    if state.mode == .command then
      return ViE.Feature.openNameInputFloat state "New Workspace" "" "ws new "
    else
      let name := s!"Workspace {wg.workspaces.size}"
      let newWs := makeWorkspaceState name none maxBufId
      let newState := state.updateCurrentWorkgroup fun wg =>
        { wg with
          workspaces := wg.workspaces.push newWs,
          currentWorkspace := wg.workspaces.size
        }
      return { newState with message := s!"Created workspace: {name}" }

    let newWs := makeWorkspaceState name none maxBufId
    let newState := state.updateCurrentWorkgroup fun wg =>
      { wg with
        workspaces := wg.workspaces.push newWs,
        currentWorkspace := wg.workspaces.size
      }
    return { newState with message := s!"Created workspace: {name}" }

    let trimmed := name.trimAscii.toString
    if trimmed.isEmpty then
      return { state with message := "Workspace name cannot be empty" }
    else
      let newWs := makeWorkspaceState trimmed none maxBufId
      let newState := state.updateCurrentWorkgroup fun wg =>
        { wg with
          workspaces := wg.workspaces.push newWs,
          currentWorkspace := wg.workspaces.size
        }
      return { newState with message := s!"Created workspace: {trimmed}" }

    let trimmed := name.trimAscii.toString
    if trimmed.isEmpty then
      return { state with message := "Workspace name cannot be empty" }
    else

    let newWs := makeWorkspaceState name (some absPath) maxBufId
    let newState := state.updateCurrentWorkgroup fun wg =>
      { wg with
        workspaces := wg.workspaces.push newWs,
        currentWorkspace := wg.workspaces.size
      }
    return { newState with message := s!"Created workspace: {name} ({absPath})" }

      let newWs := makeWorkspaceState trimmed (some absPath) maxBufId
      let newState := state.updateCurrentWorkgroup fun wg =>
        { wg with
          workspaces := wg.workspaces.push newWs,
          currentWorkspace := wg.workspaces.size
        }
      return { newState with message := s!"Created workspace: {trimmed} ({absPath})" }

def refreshActiveFileExplorer (state : EditorState) : IO EditorState := do
  let buf := state.getActiveBuffer
  match state.explorers.find? (fun (id, _) => id == buf.id) with
  | none => return state
  | some (_, explorer) =>
      if explorer.mode == .files then
        ViE.Feature.openExplorerWithPreview state explorer.currentPath explorer.previewWindowId explorer.previewBufferId
      else
        return state
def resolveCommandPath (state : EditorState) (path : String) : String :=
  if path.startsWith "/" then path else state.getCurrentWorkspace.resolvePath path

def cmdMkfile (args : List String) (state : EditorState) : IO EditorState := do
  match args with
  | [rawPath] =>
      let path := (resolveCommandPath state rawPath).trimAscii.toString
      let leaf := (System.FilePath.fileName path).getD ""
      if path.isEmpty || leaf.isEmpty then
        return { state with message := "File name cannot be empty" }
      else
        let fp := System.FilePath.mk path
        try
          if ← fp.pathExists then
            return { state with message := s!"File already exists: {path}" }
          else
            match fp.parent with
            | some p => IO.FS.createDirAll p
            | none => pure ()
            IO.FS.writeFile path ""
            let refreshed ← refreshActiveFileExplorer state
            return { refreshed with message := s!"Created file: {path}" }
        catch e =>
          return { state with message := s!"Error creating file: {e}" }
  | _ =>
      return { state with message := "Usage: :mkfile <path>" }
def cmdMkdir (args : List String) (state : EditorState) : IO EditorState := do
  match args with
  | [rawPath] =>
      let path := (resolveCommandPath state rawPath).trimAscii.toString
      let leaf := (System.FilePath.fileName path).getD ""
      if path.isEmpty || leaf.isEmpty then
        return { state with message := "Directory name cannot be empty" }
      else
        let fp := System.FilePath.mk path
        try
          if ← fp.pathExists then
            if ← fp.isDir then
              return { state with message := s!"Directory already exists: {path}" }
            else
              return { state with message := s!"File already exists: {path}" }
          else
            IO.FS.createDirAll path
            let refreshed ← refreshActiveFileExplorer state
            return { refreshed with message := s!"Created directory: {path}" }
        catch e =>
          return { state with message := s!"Error creating directory: {e}" }
  | _ =>
      return { state with message := "Usage: :mkdir <path>" }
def cmdEx (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | [] =>
      ViE.Feature.openExplorer state (state.getCurrentWorkspace.rootPath.getD ".")
  | ["list"] =>
      ViE.Feature.openExplorer state (state.getCurrentWorkspace.rootPath.getD ".")
  | ["list", path] =>
      ViE.Feature.openExplorer state path
  | [path] =>
      ViE.Feature.openExplorer state path
  | _ =>
      return { state with message := "Usage: :ex [list [path]]" }

  let path := match args with
     | [] => state.getCurrentWorkspace.rootPath.getD "."
     | [p] => p
     | _ => "."
  ViE.Feature.openExplorer state path

  cmdEx args state
def cmdBuf (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | [] => ViE.Feature.openBufferExplorer state
  | ["list"] => ViE.Feature.openBufferExplorer state
  | ["ls"] => ViE.Feature.openBufferExplorer state
  | _ => return { state with message := "Usage: :buf [list|ls]" }
def cmdBuffers (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | [] => ViE.Feature.openBufferExplorer state
  | _ => return { state with message := "Usage: :buffers" }

def cmdWgExplorer (_ : List String) (state : EditorState) : IO EditorState :=
  ViE.Feature.openWorkgroupExplorer state

def cmdWgExplorer (args : List String) (state : EditorState) : IO EditorState :=
  match args with
  | [] => cmdWg ["list"] state
  | _ => return { state with message := "Usage: :wgex" }

  ("ex", cmdEx),

  ("buf", cmdBuf),
  ("buffers", cmdBuffers),
  ("ls", cmdBuffers),
  ("mkfile", cmdMkfile),
  ("mkdir", cmdMkdir),
  ("md", cmdMkdir),

  ("redraw", cmdRedraw),
  ("redraw!", cmdRedraw),
  ("float", cmdFloat),
  ("nofloat", cmdNoFloat),
  ("floatwin", cmdFloatWin),
  ("winfloat", cmdFloatWin),
  ("wfloat", cmdFloatWin),

def openActiveAsFloating (state : EditorState) : EditorState :=
  state.updateCurrentWorkspace fun ws =>
    (ws.setWindowFloating ws.activeWindowId true).pruneFloatingWindows
def openExplorerWindowsAsFloating (state : EditorState) (previewWindowId : Option Nat) : EditorState :=
  state.updateCurrentWorkspace fun ws =>
    let ws := ws.setWindowFloating ws.activeWindowId true
    let ws :=
      match previewWindowId with
      | some wid =>
          if ws.layout.findView wid |>.isSome then
            ws.setWindowFloating wid true
          else
            ws
      | none => ws
    ws.pruneFloatingWindows
def placeExplorerInWindow (state : EditorState) (bufferId : Nat) (cursorRow : Nat) (reuseActive : Bool) : EditorState :=
  if reuseActive then
    state.updateActiveView fun v =>
      { v with bufferId := bufferId, cursor := {row := ⟨cursorRow⟩, col := 0}, scrollRow := 0, scrollCol := 0 }
  else
    let ws := state.getCurrentWorkspace
    let newWinId := ws.nextWindowId
    let s1 := ViE.Window.splitWindow state false
    s1.updateCurrentWorkspace fun ws =>
      { ws with
          activeWindowId := newWinId,
          layout := ws.layout.updateView newWinId (fun v =>
            { v with bufferId := bufferId, cursor := {row := ⟨cursorRow⟩, col := 0}, scrollRow := 0, scrollCol := 0 })
      }
def openNameInputFloat (state : EditorState) (title : String) (initialText : String) (commandPrefix : String) : EditorState :=
  let ov : FloatingOverlay := {
    title := title
    lines := #[initialText]
    maxWidth := 48
    cursorRow := 0
    cursorCol := initialText.toList.length
  }
  {
    state with
      mode := .normal
      floatingOverlay := some ov
      floatingInputCommand := some commandPrefix
      inputState := {
        state.inputState with
          commandBuffer := ""
          countBuffer := ""
          previousKey := none
          pendingKeys := ""
      }
      message := ""
      dirty := true
  }
def fileExplorerNewFileLabel : String := "[New File]"
def fileExplorerNewDirectoryLabel : String := "[New Directory]"
def isFileExplorerActionEntry (entry : FileEntry) : Bool :=
  entry.name == fileExplorerNewFileLabel || entry.name == fileExplorerNewDirectoryLabel
def fileExplorerActionEntries : List FileEntry := [
  {
    name := fileExplorerNewFileLabel
    path := ""
    isDirectory := false
  },
  {
    name := fileExplorerNewDirectoryLabel
    path := ""
    isDirectory := false
  }
]
def firstNonActionEntryIndex (entries : List FileEntry) : Option Nat :=
  let rec loop (rest : List FileEntry) (idx : Nat) : Option Nat :=
    match rest with
    | [] => none
    | e :: tail =>
        if isFileExplorerActionEntry e then
          loop tail (idx + 1)
        else
          some idx
  loop entries 0
def defaultExplorerCursorRow (entries : List FileEntry) : Nat :=
  match firstNonActionEntryIndex entries with
  | some idx => 2 + idx
  | none => 2
def ensureTrailingSlash (path : String) : String :=
  if path.endsWith "/" then path else path ++ "/"

def bufferEntryPrefix : String := "buffer://"
def makeBufferEntryPath (bufferId : Nat) : String :=
  s!"{bufferEntryPrefix}{bufferId}"
def parseBufferEntryId (path : String) : Option Nat :=
  if path.startsWith bufferEntryPrefix then
    (path.drop bufferEntryPrefix.length).toString.toNat?
  else
    none
def selectedBufferIdFromExplorer (state : EditorState) (explorer : ExplorerState) : Option Nat :=
  match getSelectedEntry state explorer with
  | none => none
  | some entry =>
      match parseBufferEntryId entry.path with
      | none => none
      | some bid =>
          let ws := state.getCurrentWorkspace
          if ws.buffers.any (fun b => b.id == bid) then
            some bid
          else
            none
def bufferExplorerLabel (buf : FileBuffer) : String :=
  let name := buf.filename.getD s!"[No Name:{buf.id}]"
  let dirty := if buf.dirty then " [+]" else ""
  s!"[{buf.id}] {name}{dirty}"

          if entry.isDirectory then

          if isFileExplorerActionEntry entry then
            return state
          else if entry.isDirectory then

      | .buffers =>
          match selectedBufferIdFromExplorer state explorer with
          | none => return state
          | some previewBufId =>
              let s1 := state.updateCurrentWorkspace fun ws =>
                { ws with layout := ws.layout.updateView previewWinId (fun v =>
                  { v with bufferId := previewBufId, cursor := Point.zero, scrollRow := 0, scrollCol := 0 }) }
              let s2 := updateExplorerState s1 bufId (fun ex => { ex with previewBufferId := none })
              return s2

        let entryOpt := getSelectedEntry s1 explorer

        let selected := getSelectedEntry s1 explorer
        let entryOpt : Option FileEntry :=
          match selected with
          | some e =>
              if isFileExplorerActionEntry e then
                explorer.entries.find? (fun x => !isFileExplorerActionEntry x)
              else
                some e
          | none =>
              explorer.entries.find? (fun x => !isFileExplorerActionEntry x)

          if entry.isDirectory then

            if entry.isDirectory then
              let content : TextBuffer := #[#[]]
              let buildLeafBits := s1.config.searchBloomBuildLeafBits
              let buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some "preview://") content buildLeafBits with dirty := false }
              let (pid, s2) := ViE.Buffer.addBuffer s1 buf
              pure (s2, pid)
            else
              ensurePreviewBuffer s1 explorer entry
        | none =>

          else
            ensurePreviewBuffer s1 explorer entry
        | none =>
          let content : TextBuffer := #[#[]]
          let buildLeafBits := s1.config.searchBloomBuildLeafBits
          let buf := { ViE.Buffer.fileBufferFromTextBufferWithConfig 0 (some "preview://") content buildLeafBits with dirty := false }
          let (pid, s2) := ViE.Buffer.addBuffer s1 buf
          pure (s2, pid)

      | .buffers =>
        let fallbackBufId :=
          match explorer.entries.find? (fun e => (parseBufferEntryId e.path).isSome) with
          | some e => (parseBufferEntryId e.path).getD s1.getActiveBuffer.id
          | none => s1.getActiveBuffer.id
        let previewBufId := (selectedBufferIdFromExplorer s1 explorer).getD fallbackBufId
        pure (s1, previewBufId)

      { ex with previewWindowId := some previewWinId, previewBufferId := some previewBufId })
    return s4

      {
        ex with
          previewWindowId := some previewWinId
          previewBufferId := if explorer.mode == .buffers then none else some previewBufId
      })
    return openExplorerWindowsAsFloating s4 (some previewWinId)

        | some newLayout => { ws with layout := newLayout }
        | none => ws

        | some newLayout => ({ ws with layout := newLayout }).pruneFloatingWindows
        | none => ws.pruneFloatingWindows

            return { s4 with message := "Preview opened" }

            let s5 := openExplorerWindowsAsFloating s4 (some previewWinId)
            return { s5 with message := "Preview opened" }

          return { s4 with message := "Preview opened" }

          let s5 := openExplorerWindowsAsFloating s4 (some previewWinId)
          return { s5 with message := "Preview opened" }

          return { s4 with message := "Preview opened" }

          let s5 := openExplorerWindowsAsFloating s4 (some previewWinId)
          return { s5 with message := "Preview opened" }
      | .buffers =>
          match selectedBufferIdFromExplorer state explorer with
          | none =>
              return { state with message := "Preview: no buffer selection" }
          | some previewBufId =>
              let ws := state.getCurrentWorkspace
              let previewWinId := ws.nextWindowId
              let s1 := ViE.Window.splitWindow state false
              let s2 := s1.updateCurrentWorkspace fun ws =>
                { ws with layout := ws.layout.updateView previewWinId (fun v =>
                  { v with bufferId := previewBufId, cursor := Point.zero, scrollRow := 0, scrollCol := 0 }) }
              let s3 := updateExplorerState s2 bufId (fun ex => { ex with previewWindowId := some previewWinId, previewBufferId := none })
              let s4 := openExplorerWindowsAsFloating s3 (some previewWinId)
              return { s4 with message := "Preview opened" }

    let mut fileEntries : List FileEntry := []

    let mut navEntries : List FileEntry := []

      fileEntries := fileEntries ++ [{

      navEntries := navEntries ++ [{

      fileEntries := fileEntries ++ [{

      navEntries := navEntries ++ [{

    let sortedEntries := fileEntries.toArray.qsort fun a b =>

    let sortedEntries := navEntries.toArray.qsort fun a b =>

    let allEntries := fileExplorerActionEntries ++ sortedEntries.toList

      entries := sortedEntries.toList

      entries := allEntries

      let icon := if entry.isDirectory then state.config.dirIcon else state.config.fileIcon
      let suffix := if entry.isDirectory then "/" else ""

      let isAction := isFileExplorerActionEntry entry
      let icon :=
        if isAction then ""
        else if entry.isDirectory then state.config.dirIcon
        else state.config.fileIcon
      let suffix := if !isAction && entry.isDirectory then "/" else ""

    -- Switch to explorer buffer
    let s''' := s''.updateActiveView fun v => { v with bufferId := bufferId, cursor := {row := 2, col := 0}, scrollRow := 0, scrollCol := 0 }

    -- Open explorer in a dedicated window by default; reuse active only when already in explorer.
    let reuseActive := state.explorers.any (fun (id, _) => id == state.getActiveBuffer.id)
    let s''' := placeExplorerInWindow s'' bufferId (defaultExplorerCursorRow explorerState.entries) reuseActive

    let s''''' := openActiveAsFloating s''''

    return (← openExplorerDefaultPreview s'''' bufferId explorerState)

    return (← openExplorerDefaultPreview s''''' bufferId explorerState)

    let mut fileEntries : List FileEntry := []

    let mut navEntries : List FileEntry := []

      fileEntries := fileEntries ++ [{

      navEntries := navEntries ++ [{

      fileEntries := fileEntries ++ [{

      navEntries := navEntries ++ [{

    let sortedEntries := fileEntries.toArray.qsort fun a b =>

    let sortedEntries := navEntries.toArray.qsort fun a b =>

    let allEntries := fileExplorerActionEntries ++ sortedEntries.toList

      entries := sortedEntries.toList

      entries := allEntries

      let icon := if entry.isDirectory then state.config.dirIcon else state.config.fileIcon
      let suffix := if entry.isDirectory then "/" else ""

      let isAction := isFileExplorerActionEntry entry
      let icon :=
        if isAction then ""
        else if entry.isDirectory then state.config.dirIcon
        else state.config.fileIcon
      let suffix := if !isAction && entry.isDirectory then "/" else ""

    let s''' := s''.updateActiveView fun v => { v with bufferId := bufferId, cursor := {row := 2, col := 0}, scrollRow := 0, scrollCol := 0 }

    let reuseActive := state.explorers.any (fun (id, _) => id == state.getActiveBuffer.id)
    let s''' := placeExplorerInWindow s'' bufferId (defaultExplorerCursorRow explorerState.entries) reuseActive

    let s''''' := openActiveAsFloating s''''

    | some _ => refreshExplorerPreview s''''
    | none => openExplorerDefaultPreview s'''' bufferId explorerState