lastFindChar : Option Char := none
  lastFindForward : Bool := true
  lastFindTill : Bool := false

  jumpBack : List Point := []
  jumpForward : List Point := []

  cursors : List (Nat × Nat) -- Row, Col per file

  cursors : List (Row × Col)

      let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val |>.getD 0

      let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row p1.col |>.getD 0

      let endOff := ViE.getOffsetFromPointInBuffer buffer p2.row.val endCol |>.getD buffer.table.tree.length

      let endOff := ViE.getOffsetFromPointInBuffer buffer p2.row ⟨endCol⟩ |>.getD buffer.table.tree.length

            let start := ViE.getOffsetFromPointInBuffer buffer r minCol |>.getD (lineStart + lineLen)

            let start := ViE.getOffsetFromPointInBuffer buffer ⟨r⟩ ⟨minCol⟩ |>.getD (lineStart + lineLen)

            let endOff := ViE.getOffsetFromPointInBuffer buffer r endCol |>.getD (lineStart + lineLen)

            let endOff := ViE.getOffsetFromPointInBuffer buffer ⟨r⟩ ⟨endCol⟩ |>.getD (lineStart + lineLen)

        let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val |>.getD 0

        let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row p1.col |>.getD 0

        let endOff := ViE.getOffsetFromPointInBuffer buffer p2.row.val endCol |>.getD buffer.table.tree.length

        let endOff := ViE.getOffsetFromPointInBuffer buffer p2.row ⟨endCol⟩ |>.getD buffer.table.tree.length

  ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0

  ViE.getOffsetFromPointInBufferWithTabStop buf cursor.row cursor.col s.config.tabStop |>.getD 0

  let (r, c) := buf.table.getPointFromOffset offset
  s.setCursor { row := ⟨r⟩, col := ⟨c⟩ }

  let p := ViE.getPointFromOffsetInBufferWithTabStop buf offset s.config.tabStop
  s.setCursor p

          let s' := applyMatchOffset s off

          let s' := applyMatchOffset (s.pushJumpPoint) off

def EditorState.searchWordUnderCursor (s : EditorState) (direction : SearchDirection) : EditorState :=
  match s.wordUnderCursor with
  | none => { s with message := "No keyword under cursor" }
  | some word =>
      let s1 := s.pushJumpPoint
      let cursor := s1.getCursor
      let cursorOffset :=
        ViE.getOffsetFromPointInBufferWithTabStop s1.getActiveBuffer cursor.row cursor.col s1.config.tabStop |>.getD 0
      let s2 := ViE.startOrUpdateSearch s1 word direction false
      let s3 :=
        match s2.searchState with
        | none => s2
        | some st => { s2 with searchState := some { st with lastMatch := some cursorOffset } }
      ViE.findNextMatch s3 (some direction)

      s

      { s with searchState := none, message := "", dirty := true }

def EditorState.jumpToColumn (s : EditorState) (col : Nat) : EditorState :=

def EditorState.jumpToColumn (s : EditorState) (col : Col) : EditorState :=

  let newCol : Col := ⟨min (col - 1) len⟩ -- 1-indexed to 0-indexed, clamped

  let newCol : Col := ⟨min (col.val - 1) len⟩ -- 1-indexed to 0-indexed, clamped

def jumpListLimit : Nat := 256
def visibleContentRows (s : EditorState) : Nat :=
  let (h, _) := s.getActiveWindowScrollBounds
  if h > 1 then h - 1 else 1
def maxScrollableTop (buffer : FileBuffer) (rowsInView : Nat) : Nat :=
  if buffer.lineCount > rowsInView then buffer.lineCount - rowsInView else 0
def clampPointToActiveBuffer (s : EditorState) (p : Point) : Point :=
  let buffer := s.getActiveBuffer
  if buffer.lineCount == 0 then
    Point.zero
  else
    let rowVal := min p.row.val (buffer.lineCount - 1)
    let tabStop := s.config.tabStop
    let lineLen := lineDisplayWidth tabStop buffer ⟨rowVal⟩
    let colVal := min p.col.val lineLen
    { row := ⟨rowVal⟩, col := ⟨colVal⟩ }
def EditorState.pushJumpPoint (s : EditorState) : EditorState :=
  let p := s.getCursor
  match s.jumpBack with
  | head :: _ =>
      if head == p then
        s
      else
        { s with jumpBack := (p :: s.jumpBack).take jumpListLimit, jumpForward := [] }
  | [] =>
      { s with jumpBack := [p], jumpForward := [] }
def EditorState.jumpBackInList (s : EditorState) : EditorState :=
  match s.jumpBack with
  | [] => { s with message := "Jump list empty" }
  | p :: rest =>
      let current := s.getCursor
      let target := clampPointToActiveBuffer s p
      let s' := s.setCursor target
      { s' with
        jumpBack := rest
        jumpForward := (current :: s.jumpForward).take jumpListLimit
      }
def EditorState.jumpForwardInList (s : EditorState) : EditorState :=
  match s.jumpForward with
  | [] => { s with message := "Jump list empty" }
  | p :: rest =>
      let current := s.getCursor
      let target := clampPointToActiveBuffer s p
      let s' := s.setCursor target
      { s' with
        jumpForward := rest
        jumpBack := (current :: s.jumpBack).take jumpListLimit
      }
def EditorState.scrollDownRows (s : EditorState) (rows : Nat) : EditorState :=
  let buffer := s.getActiveBuffer
  if buffer.lineCount == 0 then
    s
  else
    let tabStop := s.config.tabStop
    let (sRow, sCol) := s.getScroll
    let cursor := s.getCursor
    let rowsInView := visibleContentRows s
    let maxTop := maxScrollableTop buffer rowsInView
    let newTop := min (sRow.val + rows) maxTop
    let visRow := if cursor.row.val >= sRow.val then cursor.row.val - sRow.val else 0
    let newRowVal := min (newTop + visRow) (buffer.lineCount - 1)
    let newLen := lineDisplayWidth tabStop buffer ⟨newRowVal⟩
    let newColVal := min cursor.col.val newLen
    (s.setScroll ⟨newTop⟩ sCol).setCursor { row := ⟨newRowVal⟩, col := ⟨newColVal⟩ }
def EditorState.scrollUpRows (s : EditorState) (rows : Nat) : EditorState :=
  let buffer := s.getActiveBuffer
  if buffer.lineCount == 0 then
    s
  else
    let tabStop := s.config.tabStop
    let (sRow, sCol) := s.getScroll
    let cursor := s.getCursor
    let newTop := if rows > sRow.val then 0 else sRow.val - rows
    let visRow := if cursor.row.val >= sRow.val then cursor.row.val - sRow.val else 0
    let newRowVal := min (newTop + visRow) (buffer.lineCount - 1)
    let newLen := lineDisplayWidth tabStop buffer ⟨newRowVal⟩
    let newColVal := min cursor.col.val newLen
    (s.setScroll ⟨newTop⟩ sCol).setCursor { row := ⟨newRowVal⟩, col := ⟨newColVal⟩ }
def halfPageRows (s : EditorState) : Nat :=
  max 1 ((visibleContentRows s) / 2)
def fullPageRows (s : EditorState) : Nat :=
  max 1 (visibleContentRows s)
def EditorState.scrollHalfPageDown (s : EditorState) (count : Nat := 0) : EditorState :=
  let rows := if count == 0 then halfPageRows s else count
  s.scrollDownRows rows
def EditorState.scrollHalfPageUp (s : EditorState) (count : Nat := 0) : EditorState :=
  let rows := if count == 0 then halfPageRows s else count
  s.scrollUpRows rows
def EditorState.scrollPageDown (s : EditorState) (count : Nat := 0) : EditorState :=
  let rows := if count == 0 then fullPageRows s else count
  s.scrollDownRows rows
def EditorState.scrollPageUp (s : EditorState) (count : Nat := 0) : EditorState :=
  let rows := if count == 0 then fullPageRows s else count
  s.scrollUpRows rows
def EditorState.scrollWindowDown (s : EditorState) (count : Nat := 1) : EditorState :=
  let rows := if count == 0 then 1 else count
  s.scrollDownRows rows
def EditorState.scrollWindowUp (s : EditorState) (count : Nat := 1) : EditorState :=
  let rows := if count == 0 then 1 else count
  s.scrollUpRows rows
def firstNonBlankColWithTabStop (line : String) (tabStop : Nat) : Nat :=
  let rec loop (cs : List Char) (col : Nat) : Nat :=
    match cs with
    | [] => 0
    | c :: rest =>
      if c == ' ' || c == '\t' then
        loop rest (col + ViE.Unicode.charWidthAt tabStop col c)
      else
        col
  loop line.toList 0
def EditorState.moveToScreenTop (s : EditorState) (count : Nat := 0) : EditorState :=
  let buffer := s.getActiveBuffer
  if buffer.lineCount == 0 then
    s
  else
    let n := if count == 0 then 1 else count
    let rowsInView := visibleContentRows s
    let offset := min (n - 1) (rowsInView - 1)
    let (sRow, _) := s.getScroll
    let rowVal := min (sRow.val + offset) (buffer.lineCount - 1)
    let tabStop := s.config.tabStop
    let lineStr := lineString buffer ⟨rowVal⟩
    let colVal := firstNonBlankColWithTabStop lineStr tabStop
    s.setCursor { row := ⟨rowVal⟩, col := ⟨colVal⟩ }
def EditorState.moveToScreenMiddle (s : EditorState) : EditorState :=
  let buffer := s.getActiveBuffer
  if buffer.lineCount == 0 then
    s
  else
    let rowsInView := visibleContentRows s
    let offset := rowsInView / 2
    let (sRow, _) := s.getScroll
    let rowVal := min (sRow.val + offset) (buffer.lineCount - 1)
    let tabStop := s.config.tabStop
    let lineStr := lineString buffer ⟨rowVal⟩
    let colVal := firstNonBlankColWithTabStop lineStr tabStop
    s.setCursor { row := ⟨rowVal⟩, col := ⟨colVal⟩ }
def EditorState.moveToScreenBottom (s : EditorState) (count : Nat := 0) : EditorState :=
  let buffer := s.getActiveBuffer
  if buffer.lineCount == 0 then
    s
  else
    let n := if count == 0 then 1 else count
    let rowsInView := visibleContentRows s
    let fromBottom := min (n - 1) (rowsInView - 1)
    let offset := (rowsInView - 1) - fromBottom
    let (sRow, _) := s.getScroll
    let rowVal := min (sRow.val + offset) (buffer.lineCount - 1)
    let tabStop := s.config.tabStop
    let lineStr := lineString buffer ⟨rowVal⟩
    let colVal := firstNonBlankColWithTabStop lineStr tabStop
    s.setCursor { row := ⟨rowVal⟩, col := ⟨colVal⟩ }
private def findCharForwardOnLineCore
    (tabStop : Nat) (lineStr : String) (lineLen : Nat) (col : Nat) (target : Char) (fuel : Nat) : Option Nat :=
  match fuel with
  | 0 => none
  | fuel + 1 =>
      if col >= lineLen then
        none
      else
        let c := charAtDisplayCol tabStop lineStr ⟨col⟩
        if c == target then
          some col
        else
          let next := ViE.Unicode.nextDisplayColWithTabStop lineStr tabStop col
          if next <= col then none else findCharForwardOnLineCore tabStop lineStr lineLen next target fuel
private def findCharBackwardOnLineCore
    (tabStop : Nat) (lineStr : String) (col : Nat) (target : Char) (fuel : Nat) : Option Nat :=
  match fuel with
  | 0 => none
  | fuel + 1 =>
      let c := charAtDisplayCol tabStop lineStr ⟨col⟩
      if c == target then
        some col
      else if col == 0 then
        none
      else
        let prev := ViE.Unicode.prevDisplayColWithTabStop lineStr tabStop col
        if prev >= col then none else findCharBackwardOnLineCore tabStop lineStr prev target fuel
def EditorState.findCharMotion (s : EditorState) (target : Char) (forward : Bool) (till : Bool)
    (count : Nat := 1) (updateLast : Bool := true) : EditorState :=
  let buffer := s.getActiveBuffer
  let cursor := s.getCursor
  let tabStop := s.config.tabStop
  let lineStr := lineString buffer cursor.row
  let lineLen := lineDisplayWidth tabStop buffer cursor.row
  if lineLen == 0 then
    s
  else
    let n := if count == 0 then 1 else count
    let rec findNth (fromCol : Nat) (remaining : Nat) (fuel : Nat) : Option Nat :=
      match remaining with
      | 0 => some fromCol
      | rem + 1 =>
          if fuel == 0 then
            none
          else
            let found :=
              if forward then
                let start := ViE.Unicode.nextDisplayColWithTabStop lineStr tabStop fromCol
                if start >= lineLen then none
                else findCharForwardOnLineCore tabStop lineStr lineLen start target (lineLen + 1)
              else
                if fromCol == 0 then none
                else
                  let start := ViE.Unicode.prevDisplayColWithTabStop lineStr tabStop fromCol
                  if start >= lineLen then none
                  else findCharBackwardOnLineCore tabStop lineStr start target (lineLen + 1)
            match found with
            | none => none
            | some hit =>
                if rem == 0 then
                  some hit
                else
                  findNth hit rem fuel.pred
      termination_by remaining + fuel
    match findNth cursor.col.val n (lineLen + n + 1) with
    | none => { s with message := s!"Pattern not found: {target}" }
    | some hit =>
        let hitCol :=
          if till then
            if forward then
              ViE.Unicode.prevDisplayColWithTabStop lineStr tabStop hit
            else
              ViE.Unicode.nextDisplayColWithTabStop lineStr tabStop hit
          else
            hit
        let hitCol := min hitCol lineLen
        let s' := s.setCursor { cursor with col := ⟨hitCol⟩ }
        if updateLast then
          {
            s' with
              inputState := {
                s'.inputState with
                  lastFindChar := some target
                  lastFindForward := forward
                  lastFindTill := till
              }
          }
        else
          s'

def EditorState.repeatFindChar (s : EditorState) (reverse : Bool := false) : EditorState :=
  match s.inputState.lastFindChar with
  | none => { s with message := "No previous find command" }
  | some target =>
      let baseForward := s.inputState.lastFindForward
      let forward := if reverse then !baseForward else baseForward
      let count :=
        if s.inputState.lastFindTill && !reverse then 2 else 1
      s.findCharMotion target forward s.inputState.lastFindTill count false

def EditorState.wordUnderCursor (s : EditorState) : Option String :=
  let buffer := s.getActiveBuffer
  let cursor := s.getCursor
  let tabStop := s.config.tabStop
  let lineStr := lineString buffer cursor.row
  let lineLen := lineDisplayWidth tabStop buffer cursor.row
  let isWordChar (c : Char) : Bool := c.isAlphanum || c == '_'
  if lineLen == 0 || cursor.col.val >= lineLen then
    none
  else
    let curChar := charAtDisplayCol tabStop lineStr cursor.col
    if !isWordChar curChar then
      none
    else
      let rec expandLeft (col : Col) (fuel : Nat) : Col :=
        match fuel with
        | 0 => col
        | fuel + 1 =>
            if col.val == 0 then
              col
            else
              let prev := prevCol tabStop buffer cursor.row col
              let c := charAtDisplayCol tabStop lineStr prev
              if isWordChar c then expandLeft prev fuel else col
      let rec expandRightExclusive (col : Col) (fuel : Nat) : Nat :=
        match fuel with
        | 0 => col.val
        | fuel + 1 =>
            let next := nextCol tabStop buffer cursor.row col
            if next.val >= lineLen then
              lineLen
            else
              let c := charAtDisplayCol tabStop lineStr next
              if isWordChar c then
                expandRightExclusive next fuel
              else
                next.val
      let start := expandLeft cursor.col (lineLen + 1)
      let endExclusive := expandRightExclusive cursor.col (lineLen + 1)
      if endExclusive <= start.val then
        none
      else
        let sub := ViE.Unicode.dropByDisplayWidthWithTabStop lineStr.toRawSubstring tabStop start.val
        some (ViE.Unicode.takeByDisplayWidthWithTabStop sub tabStop (endExclusive - start.val))
def EditorState.jumpMatchingBracket (s : EditorState) : EditorState :=
  let buffer := s.getActiveBuffer
  let cursor := s.getCursor
  let tabStop := s.config.tabStop
  let lineLen := lineDisplayWidth tabStop buffer cursor.row
  if lineLen == 0 || cursor.col.val >= lineLen then
    { s with message := "No bracket under cursor" }
  else
    let here := charAtDisplayCol tabStop (lineString buffer cursor.row) cursor.col
    let info : Option (UInt8 × UInt8 × Bool) :=
      match here with
      | '(' => some (UInt8.ofNat 40, UInt8.ofNat 41, true)
      | '[' => some (UInt8.ofNat 91, UInt8.ofNat 93, true)
      | '{' => some (UInt8.ofNat 123, UInt8.ofNat 125, true)
      | ')' => some (UInt8.ofNat 40, UInt8.ofNat 41, false)
      | ']' => some (UInt8.ofNat 91, UInt8.ofNat 93, false)
      | '}' => some (UInt8.ofNat 123, UInt8.ofNat 125, false)
      | _ => none
    match info with
    | none => { s with message := "No bracket under cursor" }
    | some (openB, closeB, forward) =>
        let off := ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row cursor.col tabStop |>.getD 0
        let bytes := buffer.table.toString.toUTF8
        if off >= bytes.size then
          { s with message := "No bracket match" }
        else
          let rec scanForward (i : Nat) (depth : Nat) (fuel : Nat) : Option Nat :=
            match fuel with
            | 0 => none
            | fuel + 1 =>
                if i >= bytes.size then
                  none
                else
                  let b := bytes[i]!
                  let depth :=
                    if b == openB then depth + 1
                    else if b == closeB then depth - 1
                    else depth
                  if depth == 0 then some i else scanForward (i + 1) depth fuel
            termination_by fuel
          let rec scanBackward (i : Nat) (depth : Nat) (fuel : Nat) : Option Nat :=
            match fuel with
            | 0 => none
            | fuel + 1 =>
                if i == 0 then
                  none
                else
                  let j := i - 1
                  let b := bytes[j]!
                  let depth :=
                    if b == closeB then depth + 1
                    else if b == openB then depth - 1
                    else depth
                  if depth == 0 then some j else scanBackward j depth fuel
            termination_by fuel
          let hit :=
            if forward then
              scanForward (off + 1) 1 (bytes.size + 1)
            else
              scanBackward off 1 (bytes.size + 1)
          match hit with
          | none => { s with message := "No bracket match" }
          | some j =>
              let p := ViE.getPointFromOffsetInBufferWithTabStop buffer j tabStop
              s.setCursor p

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row cursor.col tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row cursor.col tabStop with

       match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val prevC.val tabStop,
             ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop with

       match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row prevC tabStop,
             ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row cursor.col tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val nextC.val tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row cursor.col tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row nextC tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val nextC.val tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row cursor.col tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row nextC tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer p1.row.val p1.col.val tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer p2.row.val p2.col.val tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer p1.row p1.col tabStop,
          ViE.getOffsetFromPointInBufferWithTabStop buffer p2.row p2.col tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val targetCol tabStop with

    match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row ⟨targetCol⟩ tabStop with

    let (offset, textToInsert) := match ViE.getOffsetFromPointInBuffer buffer row 0 with

    let (offset, textToInsert) := match ViE.getOffsetFromPointInBuffer buffer ⟨row⟩ 0 with

            let insertOff := ViE.getOffsetFromPointInBufferWithTabStop buf row lineW tabStop |>.getD (buf.table.tree.length)

            let insertOff := ViE.getOffsetFromPointInBufferWithTabStop buf ⟨row⟩ ⟨lineW⟩ tabStop |>.getD (buf.table.tree.length)

            let off' := ViE.getOffsetFromPointInBufferWithTabStop buf' row targetCol tabStop |>.getD insertOff

            let off' := ViE.getOffsetFromPointInBufferWithTabStop buf' ⟨row⟩ ⟨targetCol⟩ tabStop |>.getD insertOff

            let off := ViE.getOffsetFromPointInBufferWithTabStop buf row targetCol tabStop |>.getD 0

            let off := ViE.getOffsetFromPointInBufferWithTabStop buf ⟨row⟩ ⟨targetCol⟩ tabStop |>.getD 0

  let currentOffset := match ViE.getOffsetFromPointInBufferWithTabStop buf cursor.row.val cursor.col.val tabStop with

  let currentOffset := match ViE.getOffsetFromPointInBufferWithTabStop buf cursor.row cursor.col tabStop with

  let currentOffset := match ViE.getOffsetFromPointInBufferWithTabStop buf cursor.row.val cursor.col.val tabStop with

  let currentOffset := match ViE.getOffsetFromPointInBufferWithTabStop buf cursor.row cursor.col tabStop with

  lastFindChar := none
  lastFindForward := true
  lastFindTill := false

  jumpBack := []
  jumpForward := []

  let rawCount (state : EditorState) : Nat :=
      match state.inputState.countBuffer.toNat? with
      | some n => n
      | none => 0

    if s.inputState.previousKey == some 'f' then
      match k with
      | Key.char c =>
        let s' := { s with inputState := { s.inputState with previousKey := none } }
        let n := if s'.getCount == 0 then 1 else s'.getCount
        pure $ clearInput (EditorState.findCharMotion s' c true false n true)
      | _ =>
        pure { s with inputState := { s.inputState with previousKey := none, countBuffer := "" } }
    else if s.inputState.previousKey == some 't' then
      match k with
      | Key.char c =>
        let s' := { s with inputState := { s.inputState with previousKey := none } }
        let n := if s'.getCount == 0 then 1 else s'.getCount
        pure $ clearInput (EditorState.findCharMotion s' c true true n true)
      | _ =>
        pure { s with inputState := { s.inputState with previousKey := none, countBuffer := "" } }
    else

          searchState := none
          message := ""

          searchState := none
          message := ""

    | Key.char 'H' =>
      let n := rawCount s
      pure $ clearInput ((s.pushJumpPoint).moveToScreenTop n)
    | Key.char 'M' =>
      pure $ clearInput ((s.pushJumpPoint).moveToScreenMiddle)
    | Key.char 'L' =>
      let n := rawCount s
      pure $ clearInput ((s.pushJumpPoint).moveToScreenBottom n)
    | Key.char 'f' =>
      pure { s with inputState := { s.inputState with previousKey := some 'f' } }
    | Key.char 't' =>
      pure { s with inputState := { s.inputState with previousKey := some 't' } }
    | Key.char ';' =>
      pure $ clearInput (EditorState.repeatFindChar s false)
    | Key.char ',' =>
      pure $ clearInput (EditorState.repeatFindChar s true)
    | Key.char '%' =>
      pure $ clearInput ((s.pushJumpPoint).jumpMatchingBracket)
    | Key.char '*' =>
      pure $ clearInput (EditorState.searchWordUnderCursor s .forward)
    | Key.char '#' =>
      pure $ clearInput (EditorState.searchWordUnderCursor s .backward)

      pure $ clearInput (EditorState.jumpToColumn s n)

      pure $ clearInput (EditorState.jumpToColumn s ⟨n⟩)

    | Key.ctrl 'd' =>
      let n := rawCount s
      pure $ clearInput (EditorState.scrollHalfPageDown s n)
    | Key.ctrl 'u' =>
      let n := rawCount s
      pure $ clearInput (EditorState.scrollHalfPageUp s n)
    | Key.ctrl 'f' =>
      let n := rawCount s
      pure $ clearInput (EditorState.scrollPageDown s n)
    | Key.ctrl 'b' =>
      let n := rawCount s
      pure $ clearInput (EditorState.scrollPageUp s n)
    | Key.ctrl 'e' =>
      let n := rawCount s
      pure $ clearInput (EditorState.scrollWindowDown s n)
    | Key.ctrl 'y' =>
      let n := rawCount s
      pure $ clearInput (EditorState.scrollWindowUp s n)
    | Key.ctrl 'o' =>
      pure $ clearInput (EditorState.jumpBackInList s)
    | Key.char '\t' =>
      pure $ clearInput (EditorState.jumpForwardInList s)

        if newCmd.isEmpty then
          return {
            state with
              searchState := none
              message := ""
              dirty := true
              inputState := {
                state.inputState with
                  commandBuffer := ""
                  pendingSearch := false
              }
          }
        else

def lineRangeWithNewline (pt : PieceTable) (row : Nat) : Option (Nat × Nat) :=
  match pt.getLineRange row with

def lineRangeWithNewline (pt : PieceTable) (row : Row) : Option (Nat × Nat) :=
  match pt.getLineRange row.val with

def collectMatchesInLine (pt : PieceTable) (row : Nat) (pattern : ByteArray) : Array (Nat × Nat) :=
  match pt.getLineRange row with

def collectMatchesInLine (pt : PieceTable) (row : Row) (pattern : ByteArray) : Array (Nat × Nat) :=
  match pt.getLineRange row.val with

        let cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0

        let cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row cursor.col |>.getD 0

            let hasMatch := (collectMatchesInLine buf.table row patBytes).size > 0

            let hasMatch := (collectMatchesInLine buf.table ⟨row⟩ patBytes).size > 0

              match lineRangeWithNewline buf.table row with

              match lineRangeWithNewline buf.table ⟨row⟩ with

                    let lineMatches := collectMatchesInLine buf.table row oldBytes

                    let lineMatches := collectMatchesInLine buf.table ⟨row⟩ oldBytes

        let cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0

        let cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row cursor.col |>.getD 0

def getOffsetFromPointInBufferWithTabStop (buffer : FileBuffer) (row col tabStop : Nat) : Option Nat :=
  match buffer.table.getLineRange row with

def getOffsetFromPointInBufferWithTabStop (buffer : FileBuffer) (row : Row) (col : Col) (tabStop : Nat) : Option Nat :=
  match buffer.table.getLineRange row.val with

      let line := getLineFromBuffer buffer ⟨row⟩ |>.getD ""
      let byteOff := ViE.Unicode.displayColToByteOffsetWithTabStop line tabStop col

      let line := getLineFromBuffer buffer row |>.getD ""
      let byteOff := ViE.Unicode.displayColToByteOffsetWithTabStop line tabStop col.val

/-- Convert byte offset to Row/Col (display column) with configurable tab stop. -/
def getPointFromOffsetInBufferWithTabStop (buffer : FileBuffer) (offset tabStop : Nat) : Point :=
  let (rowNat, _) := buffer.table.getPointFromOffset offset
  match buffer.table.getLineRange rowNat with
  | some (startOff, len) =>
      let rel := if offset >= startOff then min (offset - startOff) len else 0
      let sub := ViE.PieceTree.getSubstring buffer.table.tree startOff rel buffer.table
      let col := ViE.Unicode.stringWidthWithTabStop sub tabStop
      Point.fromNat rowNat col
  | none =>
      Point.fromNat rowNat 0

def getOffsetFromPointInBuffer (buffer : FileBuffer) (row col : Nat) : Option Nat :=

def getOffsetFromPointInBuffer (buffer : FileBuffer) (row : Row) (col : Col) : Option Nat :=

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

def clampCursorInBuffer (buffer : FileBuffer) (row col : Nat) : Point :=

def clampCursorInBuffer (buffer : FileBuffer) (row : Row) (col : Col) : Point :=

  let clampedRow := if lineCount == 0 then 0 else min row (lineCount - 1)

  let clampedRow := if lineCount == 0 then 0 else min row.val (lineCount - 1)

  let clampedCol := if lineLen == 0 then 0 else min col (lineLen - 1)

  let clampedCol := if lineLen == 0 then 0 else min col.val (lineLen - 1)

  let cursor := clampCursorInBuffer activeBuf row col

  let cursor := clampCursorInBuffer activeBuf ⟨row⟩ ⟨col⟩

  let sInc0 := ViE.startOrUpdateSearch ViE.initialState "abc" .forward false
  let sInc1 := {
    sInc0 with
      mode := .searchForward
      inputState := { sInc0.inputState with commandBuffer := "" }
  }
  let sInc2 := ViE.runIncrementalSearch sInc1
  let incCleared :=
    match sInc2.searchState with
    | none => true
    | some _ => false
  assertEqual "Incremental search with empty pattern clears highlight state" true incCleared

def testVimCompatMotions : IO Unit := do
  IO.println "  Testing Vim Compatibility Motions..."
  let s0 := { ViE.initialState with windowHeight := 12, windowWidth := 80 }
  let lines := String.intercalate "\n" ((List.range 30).map (fun i => s!"  line{i}")) ++ "\n"
  let s1 ← runKeys s0 ([Key.char 'i'] ++ keys lines ++ [Key.esc] ++ keys "gg0")
  let sCd ← runKeys s1 [Key.ctrl 'd']
  assertCursor "Ctrl-d scrolls half page down" sCd 5 0
  let sCu ← runKeys sCd [Key.ctrl 'u']
  assertCursor "Ctrl-u scrolls half page up" sCu 0 0
  let sCf ← runKeys s1 [Key.ctrl 'f']
  assertCursor "Ctrl-f scrolls one page down" sCf 10 0
  let sCb ← runKeys sCf [Key.ctrl 'b']
  assertCursor "Ctrl-b scrolls one page up" sCb 0 0
  let sCe ← runKeys s1 [Key.ctrl 'e']
  let (ceRow, _) := sCe.getScroll
  assertEqual "Ctrl-e scrolls window down by one line" 1 ceRow.val
  let sCy ← runKeys sCe [Key.ctrl 'y']
  let (cyRow, _) := sCy.getScroll
  assertEqual "Ctrl-y scrolls window up by one line" 0 cyRow.val
  let sH ← runKeys sCf [Key.char 'H']
  assertCursor "H moves to top line of screen" sH 10 2
  let sM ← runKeys sCf [Key.char 'M']
  assertCursor "M moves to middle line of screen" sM 15 2
  let sL ← runKeys sCf [Key.char 'L']
  assertCursor "L moves to bottom line of screen" sL 19 2
  let sF0 ← runKeys s0 ([Key.char 'i'] ++ keys "abcaXcaYca" ++ [Key.esc] ++ [Key.char '0'])
  let sF1 ← runKeys sF0 [Key.char 'f', Key.char 'a']
  assertCursor "fa finds next character" sF1 0 3
  let sF2 ← runKeys sF1 [Key.char ';']
  assertCursor "; repeats last f motion" sF2 0 6
  let sF3 ← runKeys sF2 [Key.char ',']
  assertCursor ", reverses last f motion" sF3 0 3
  let sT1 ← runKeys sF3 [Key.char 't', Key.char 'a']
  assertCursor "ta moves before target" sT1 0 5
  let sT2 ← runKeys sT1 [Key.char ';']
  assertCursor "; repeats last t motion" sT2 0 8

  let sPct0 ← runKeys s0 ([Key.char 'i'] ++ keys "(a[b]c)" ++ [Key.esc] ++ [Key.char '0'])
  let sPct1 ← runKeys sPct0 [Key.char '%']
  assertCursor "% jumps to matching bracket" sPct1 0 6
  let sPct2 ← runKeys sPct1 [Key.ctrl 'o']
  assertCursor "Ctrl-o jumps back in jump list" sPct2 0 0
  let sPct3 ← runKeys sPct2 [Key.char '\t']
  assertCursor "Ctrl-i (Tab) jumps forward in jump list" sPct3 0 6
  let sStar0 := ViE.initialState
  let sStar1 ← runKeys sStar0 ([Key.char 'i'] ++ keys "foo bar\nfoo baz\nbar foo\n" ++ [Key.esc] ++ keys "gg0")
  let sStar2 ← runKeys sStar1 [Key.char '*']
  assertCursor "* searches next word under cursor" sStar2 1 0
  let sStar3 ← runKeys sStar2 [Key.char '#']
  assertCursor "# searches previous word under cursor" sStar3 0 0

  let s2Prompt ← runKeys s2 [Key.char '/']
  let promptCleared :=
    match s2Prompt.searchState with
    | none => true
    | some _ => false
  assertEqual "Starting new search prompt clears old search highlight state" true promptCleared

  testVimCompatMotions