WRBKZMYVNHRWT7TTUGTDJ3TMWZB32QYW5PCLKTTVAJ2YF6OI3LTAC let getBuffer (id : Nat) : FileBuffer :=wg.buffers.find? (fun b => b.id == id) |>.getD initialBuffer
let getBuffer (st : EditorState) (id : Nat) : FileBuffer :=let wg := st.getCurrentWorkgroupwg.buffers.find? (fun b => b.id == id) |>.getD initialFileBuffer
if lineIdx < FileBuffer.lineCount buf thenif let some lineStr := getLineFromBuffer buf lineIdx thenlet lnWidth := if state.config.showLineNumbers then 4 else 0let availableWidth := if w > lnWidth then w - lnWidth else 0
if lineIdx.val < FileBuffer.lineCount buf then-- Check cachelet cachedLine := buf.cache.find lineIdxlet (displayLine, nextSt) := match cachedLine with| some s => (s, currentSt)| none =>if let some lineStr := getLineFromBuffer buf lineIdx thenlet lnWidth := if st.config.showLineNumbers then 4 else 0let availableWidth := if w > lnWidth then w - lnWidth else 0let sub := lineStr.toRawSubstring.drop view.scrollCol.vallet dl := takeVisual sub availableWidth-- Update cache in currentStlet updatedBuf := { buf with cache := buf.cache.update lineIdx dl }let s' := currentSt.updateCurrentWorkgroup fun wg =>{ wg with buffers := wg.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }(dl, s')else ("", currentSt)
let isVisual := state.mode == .visual || state.mode == .visualBlocklet selRange := if isVisual then state.selectionStart else none
match selRange with| none => winBuf := winBuf ++ displayLine| some _ =>let mut styleActive := falselet chars := displayLine.toListlet mut idx := 0for ch in chars dolet colVal := view.scrollCol.val + idxlet isSelected := st.isInSelection lineIdx ⟨colVal⟩
match selRange with| none => winBuf := winBuf ++ displayLine| some _ =>let mut styleActive := false-- For highlighting, simpler to just iterate over result string or re-calculate-- This visual highlighting logic implies `displayLine` is the raw chars roughly.-- But `takeVisual` expands tabs/controls!-- Logic below assumes 1:1 char mapping which might be flawed if `takeVisual` changes string (e.g. ^A).-- Leaving visual highlight logic "as is" but it iterates `displayLine.toList`.-- `displayLine` is a String, so `toList` is fine (though allocs). Visual mode perf is secondary to normal nav.let chars := displayLine.toListlet mut idx := 0for c in chars dolet col := view.scrollCol.val + idxlet isSelected := state.isInSelection lineIdx colif isSelected && !styleActive thenwinBuf := winBuf ++ "\x1b[7m" -- Inverse videostyleActive := trueelse if !isSelected && styleActive thenwinBuf := winBuf ++ "\x1b[0m"styleActive := false
if isSelected && !styleActive thenwinBuf := winBuf ++ "\x1b[7m" -- Inverse videostyleActive := trueelse if !isSelected && styleActive thenwinBuf := winBuf ++ "\x1b[0m"styleActive := false
let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{id} B:{view.bufferId}] [WG:{state.currentGroup}] {state.workspace.displayName}"-- Ensure status line also clears restwinBuf := winBuf ++ state.config.statusBarStyle ++ statusStr.trimAscii ++ Terminal.clearLineStr ++ state.config.resetStyle
let statusStr := s!"{modeStr} {fileName}{eolMark} [W:{id} B:{view.bufferId}] [WG:{st.currentGroup}] {st.workspace.displayName}"winBuf := winBuf ++ st.config.statusBarStyle ++ statusStr.trimAscii ++ Terminal.clearLineStr ++ st.config.resetStyle
@[simp] def add (r : Row) (n : Nat) : Row := ⟨r.val + n⟩@[simp] def sub (r : Row) (n : Nat) : Row := ⟨r.val - n⟩instance : OfNat Row n := ⟨⟨n⟩⟩instance : LT Row := ⟨fun a b => a.val < b.val⟩instance : LE Row := ⟨fun a b => a.val ≤ b.val⟩instance (a b : Row) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))instance (a b : Row) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))instance : Min Row := ⟨fun a b => if a.val ≤ b.val then a else b⟩instance : Max Row := ⟨fun a b => if a.val ≥ b.val then a else b⟩instance : HAdd Row Nat Row := ⟨fun r n => ⟨r.val + n⟩⟩instance : HAdd Row Nat Nat := ⟨fun r n => r.val + n⟩instance : HSub Row Row Nat := ⟨fun a b => a.val - b.val⟩instance : HSub Row Nat Row := ⟨fun r n => ⟨r.val - n⟩⟩instance : HSub Row Nat Nat := ⟨fun r n => r.val - n⟩
instance : OfNat Row n := ⟨⟨n⟩⟩instance : LT Row := ⟨fun a b => a.val < b.val⟩instance : LE Row := ⟨fun a b => a.val ≤ b.val⟩instance (a b : Row) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))instance (a b : Row) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))instance : Min Row := ⟨fun a b => if a.val ≤ b.val then a else b⟩instance : Max Row := ⟨fun a b => if a.val ≥ b.val then a else b⟩instance : Add Row := ⟨fun a b => ⟨a.val + b.val⟩⟩instance : Sub Row := ⟨fun a b => ⟨a.val - b.val⟩⟩instance : HAdd Row Nat Row := ⟨fun r n => ⟨r.val + n⟩⟩instance : HSub Row Nat Row := ⟨fun r n => ⟨r.val - n⟩⟩instance : Coe Row Nat := ⟨(·.val)⟩instance : GetElem (List α) Row α (fun l r => r.val < l.length) wheregetElem l r h := l[r.val]instance : GetElem (Array α) Row α (fun a r => r.val < a.size) wheregetElem a r h := a[r.val]
@[simp] def add (c : Col) (n : Nat) : Col := ⟨c.val + n⟩@[simp] def sub (c : Col) (n : Nat) : Col := ⟨c.val - n⟩instance : OfNat Col n := ⟨⟨n⟩⟩instance : LT Col := ⟨fun a b => a.val < b.val⟩instance : LE Col := ⟨fun a b => a.val ≤ b.val⟩instance (a b : Col) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))instance (a b : Col) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))instance : Min Col := ⟨fun a b => if a.val ≤ b.val then a else b⟩instance : Max Col := ⟨fun a b => if a.val ≥ b.val then a else b⟩instance : HAdd Col Nat Col := ⟨fun c n => ⟨c.val + n⟩⟩instance : HAdd Col Nat Nat := ⟨fun c n => c.val + n⟩instance : HSub Col Nat Col := ⟨fun c n => ⟨c.val - n⟩⟩instance : HSub Col Col Nat := ⟨fun a b => a.val - b.val⟩
instance : OfNat Col n := ⟨⟨n⟩⟩instance : LT Col := ⟨fun a b => a.val < b.val⟩instance : LE Col := ⟨fun a b => a.val ≤ b.val⟩instance (a b : Col) : Decidable (a < b) := inferInstanceAs (Decidable (a.val < b.val))instance (a b : Col) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.val ≤ b.val))instance : Min Col := ⟨fun a b => if a.val ≤ b.val then a else b⟩instance : Max Col := ⟨fun a b => if a.val ≥ b.val then a else b⟩instance : Add Col := ⟨fun a b => ⟨a.val + b.val⟩⟩instance : Sub Col := ⟨fun a b => ⟨a.val - b.val⟩⟩instance : HAdd Col Nat Col := ⟨fun c n => ⟨c.val + n⟩⟩instance : HSub Col Nat Col := ⟨fun c n => ⟨c.val - n⟩⟩instance : Coe Col Nat := ⟨(·.val)⟩instance : GetElem (List α) Col α (fun l c => c.val < l.length) wheregetElem l c h := l[c.val]instance : GetElem (Array α) Col α (fun a c => c.val < a.size) wheregetElem a c h := a[c.val]
structure RenderCache where/-- Visual string for a line, cached to avoid re-calculating widths/tabs/etc. -/lineMap : List (Row × String)deriving Inhabitednamespace RenderCachedef find (c : RenderCache) (r : Row) : Option String :=c.lineMap.find? (fun (row, _) => row == r) |>.map (fun (_, s) => s)def update (c : RenderCache) (r : Row) (s : String) : RenderCache :=-- Simple prepend and filter to keep it fresh. In a real editor we might want to cap the size.let newMap := (r, s) :: (c.lineMap.filter (fun (row, _) => row != r)){ lineMap := if newMap.length > 200 then newMap.take 200 else newMap }end RenderCache
if row < p1.row.val || row > p2.row.val then falseelse if row > p1.row.val && row < p2.row.val then trueelse if p1.row.val == p2.row.val then col >= p1.col.val && col <= p2.col.valelse if row == p1.row.val then col >= p1.col.valelse if row == p2.row.val then col <= p2.col.val
if row < p1.row || row > p2.row then falseelse if row > p1.row && row < p2.row then trueelse if p1.row == p2.row then col >= p1.col && col <= p2.colelse if row == p1.row then col >= p1.colelse if row == p2.row then col <= p2.col
let minRow := min startPt.row cursor.rowlet maxRow := max startPt.row cursor.rowlet minCol := min startPt.col cursor.collet maxCol := max startPt.col cursor.collet content := s.activeBufferContent(List.range (maxRow.val - minRow.val + 1)).toArray.map fun i =>let row := minRow.val + ilet line := getLine content row |>.getD ""let chars := line.toListstringToLine (String.ofList (chars.drop minCol.val |>.take (maxCol.val - minCol.val + 1)))
let minRow := (min startPt.row cursor.row).vallet maxRow := (max startPt.row cursor.row).vallet minCol := (min startPt.col cursor.col).vallet maxCol := (max startPt.col cursor.col).vallet lines := (List.range (maxRow - minRow + 1)).map fun i =>let r := minRow + ilet line := ViE.getLineFromBuffer buffer ⟨r⟩ |>.getD ""let sub := line.toRawSubstring.drop minCol |>.take (maxCol - minCol + 1)sub.toStringString.intercalate "\n" lines
let content := s.activeBufferContentif p1.row == p2.row thenlet line := getLine content p1.row.val |>.getD ""let chars := line.toList#[stringToLine (String.ofList (chars.drop p1.col.val |>.take (p2.col.val - p1.col.val + 1)))]elselet firstLine := getLine content p1.row.val |>.getD ""let lastLine := getLine content p2.row.val |>.getD ""let midLines := arrayDrop (arrayTake content p2.row.val) (p1.row.val + 1)let firstPart := stringToLine (String.ofList (firstLine.toList.drop p1.col.val))let lastPart := stringToLine (String.ofList (lastLine.toList.take (p2.col.val + 1)))arrayConcat [#[firstPart], midLines, #[lastPart]]
let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.lengthPieceTable.PieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.table
let minRow := min startPt.row cursor.rowlet maxRow := max startPt.row cursor.rowlet minCol := min startPt.col cursor.collet maxCol := max startPt.col cursor.collet s' := s.updateActiveBufferContent fun buffer =>buffer.mapIdx fun i lineArr =>let line := lineToString lineArrif i >= minRow.val && i <= maxRow.val thenlet chars := line.toListif minCol.val < chars.length thenlet before := chars.take minCol.vallet after := chars.drop (maxCol.val + 1)stringToLine (String.ofList (before ++ after))elselineArrelselineArr(s'.setCursor (Point.make minRow.val minCol.val)).exitVisualMode
let minRow := (min startPt.row cursor.row).vallet maxRow := (max startPt.row cursor.row).vallet minCol := (min startPt.col cursor.col).vallet maxCol := (max startPt.col cursor.col).vallet s' := (List.range (maxRow - minRow + 1)).foldl (init := s) fun st i =>let r := minRow + ist.updateActiveBuffer fun buffer =>match buffer.table.getLineRange r with| some (lineStart, lineLen) =>let start := lineStart + minCollet len := min (maxCol - minCol + 1) (if lineLen > minCol then lineLen - minCol else 0)if len > 0 then{ buffer with table := buffer.table.delete start len start, dirty := true }else buffer| none => buffers'.exitVisualMode |>.setCursor { row := ⟨minRow⟩, col := ⟨minCol⟩ }
let s' := s.updateActiveBufferContent fun buffer =>if p1.row == p2.row thenmodifyLine buffer p1.row.val fun line =>let chars := line.toListlet before := chars.take p1.col.vallet after := chars.drop (p2.col.val + 1)String.ofList (before ++ after)elselet beforeLines := arrayTake buffer p1.row.vallet afterLines := arrayDrop buffer (p2.row.val + 1)let firstLine := getLine buffer p1.row.val |>.getD ""let lastLine := getLine buffer p2.row.val |>.getD ""let newJoinedLine := stringToLine (String.ofList (firstLine.toList.take p1.col.val ++ lastLine.toList.drop (p2.col.val + 1)))arrayConcat [beforeLines, #[newJoinedLine], afterLines](s'.setCursor p1).exitVisualMode
let s' := s.updateActiveBuffer fun buffer =>let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.length{ buffer with table := buffer.table.delete startOff (endOff - startOff) startOff, dirty := true }s'.exitVisualMode |>.setCursor p1
let newRow := cursor.row.val - 1let lineLen := getLineLengthFromBuffer s.getActiveBuffer newRow |>.getD 0s.setCursor (Point.make newRow (min cursor.col.val lineLen))
let newRow : Row := ⟨cursor.row.val - 1⟩let lineLen := ViE.getLineLengthFromBuffer s.getActiveBuffer newRow |>.getD 0s.setCursor { cursor with row := newRow, col := ⟨min cursor.col.val lineLen⟩ }
let newRow := cursor.row.val + 1let lineLen := getLineLengthFromBuffer buffer newRow |>.getD 0s.setCursor (Point.make newRow (min cursor.col.val lineLen))
let newRow : Row := ⟨cursor.row.val + 1⟩let lineLen := ViE.getLineLengthFromBuffer buffer newRow |>.getD 0s.setCursor { cursor with row := newRow, col := ⟨min cursor.col.val lineLen⟩ }
let len := getLineLengthFromBuffer s.getActiveBuffer cursor.row.val |>.getD 0let newCol := min (col - 1) len -- 1-indexed to 0-indexed, clampedlet s' := s.setCursor (Point.make cursor.row.val newCol)
let len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0let newCol : Col := ⟨min (col - 1) len⟩ -- 1-indexed to 0-indexed, clampedlet s' := s.setCursor { cursor with col := newCol }
let newRow := if line == 0 then 0 else min (line - 1) (maxLine - 1)let lineLen := getLineLengthFromBuffer buffer newRow |>.getD 0
let newRowVal := if line == 0 then 0 else min (line - 1) (maxLine - 1)let newRow : Row := ⟨newRowVal⟩let lineLen := ViE.getLineLengthFromBuffer buffer newRow |>.getD 0
let cursor := s.getCursorlet len := ViE.getLineLengthFromBuffer s.getActiveBuffer cursor.row |>.getD 0match s.mode with| Mode.insert =>if cursor.col.val > len thens.setCursor { cursor with col := ⟨len⟩ }elses| _ => -- Normal, Visual etc.if len == 0 thens.setCursor { cursor with col := ⟨0⟩ }else if cursor.col.val >= len thens.setCursor { cursor with col := ⟨len - 1⟩ }elsesdef isKeyword (c : Char) : Bool :=c.isAlphanum || c == '_'mutualpartial def findNextForward (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) : Row × Col :=let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0if lineLen == 0 then(row, 0) -- Stop at empty lineelse if col.val >= lineLen then-- End of line, wrap to next lineif row.val + 1 < FileBuffer.lineCount buffer thenlet nextRow := row.succlet nextLen := ViE.getLineLengthFromBuffer buffer nextRow |>.getD 0if nextLen == 0 then(nextRow, 0) -- Stop at empty lineelsefindNextForward buffer nextRow 0 trueelse(row, col) -- End of fileelselet lineStr := ViE.getLineFromBuffer buffer row |>.getD ""let c := List.getD lineStr.toList col.val ' 'let isKw := isKeyword clet isSpace := c.isWhitespaceif !started thenif isSpace thenfindNextForward buffer row col.succ trueelsefindNextWordEndForward buffer row col.succ isKwelseif isSpace thenfindNextForward buffer row col.succ startedelse(row, col) -- Found start of next wordpartial def findNextWordEndForward (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) : Row × Col :=let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0if col.val >= lineLen thenif row.val + 1 < FileBuffer.lineCount buffer thenfindNextForward buffer row.succ 0 trueelse(row, col)elselet lineStr := ViE.getLineFromBuffer buffer row |>.getD ""let c := List.getD lineStr.toList col.val ' 'let isKw := isKeyword clet isSpace := c.isWhitespaceif isSpace thenfindNextForward buffer row col.succ trueelse if isKw != wasTv then(row, col)elsefindNextWordEndForward buffer row col.succ wasTvend/-- Move forward to start of next word (w) -/def EditorState.moveWordForward (s : EditorState) : EditorState :=let buffer := s.getActiveBuffer
let len := getLineLengthFromBuffer s.getActiveBuffer cursor.row.val |>.getD 0if cursor.col.val > len thens.setCursor (Point.make cursor.row.val len)
let currLineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0let (r, c) := if currLineLen == 0 thenif cursor.row.val + 1 < FileBuffer.lineCount buffer thenfindNextForward buffer cursor.row.succ 0 trueelse(cursor.row, 0)elselet lineStr := ViE.getLineFromBuffer buffer cursor.row |>.getD ""if cursor.col.val < currLineLen thenlet ch := List.getD lineStr.toList cursor.col.val ' 'let isKw := isKeyword chlet isSpace := ch.isWhitespaceif isSpace thenfindNextForward buffer cursor.row cursor.col.succ trueelsefindNextWordEndForward buffer cursor.row cursor.col.succ isKwelseif cursor.row.val + 1 < FileBuffer.lineCount buffer thenfindNextForward buffer cursor.row.succ 0 trueelse(cursor.row, ⟨currLineLen⟩)let finalLineLen := ViE.getLineLengthFromBuffer buffer r |>.getD 0let finalColVal := if r.val + 1 >= FileBuffer.lineCount buffer && c.val >= finalLineLen && finalLineLen > 0 && s.mode != Mode.insert thenfinalLineLen - 1elsemin c.val finalLineLens.setCursor { row := r, col := ⟨finalColVal⟩ }mutualpartial def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""let c := List.getD lineStr.toList col.val ' 'if c.isWhitespace thenif col.val == 0 thenif row.val > 0 thenlet prevRow := row.predlet prevLen := ViE.getLineLengthFromBuffer buffer prevRow |>.getD 0if prevLen > 0 then findPrevStart buffer prevRow ⟨prevLen - 1⟩ else (prevRow, 0)else (0, 0)elsefindPrevStart buffer row col.predelselet isKw := isKeyword cconsumeWordBackward buffer row col isKwpartial def consumeWordBackward (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""let c := List.getD lineStr.toList col.val ' 'let isKw := isKeyword cif c.isWhitespace || isKw != wantKw then(row, col.succ)elseif col.val == 0 then (row, 0)else consumeWordBackward buffer row col.pred wantKwend/-- Move backward to start of previous word (b) -/def EditorState.moveWordBackward (s : EditorState) : EditorState :=let buffer := s.getActiveBufferlet cursor := s.getCursorif cursor.row.val == 0 && cursor.col.val == 0 then s
s
let lineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0let startCol : Col := if cursor.col.val >= lineLen then ⟨lineLen⟩ else cursor.collet (r, c) :=if startCol.val == 0 thenif cursor.row.val > 0 thenlet prevRow := cursor.row.predlet prevLen := ViE.getLineLengthFromBuffer buffer prevRow |>.getD 0if prevLen > 0 thenfindPrevStart buffer prevRow ⟨prevLen - 1⟩else(prevRow, 0)else (0, 0)elsefindPrevStart buffer cursor.row startCol.preds.setCursor { row := r, col := c }mutualpartial def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0if col.val >= lineLen thenif row.val + 1 < FileBuffer.lineCount buffer thenfindNextEnd buffer row.succ 0else(row, col)elselet lineStr := ViE.getLineFromBuffer buffer row |>.getD ""let c := List.getD lineStr.toList col.val ' 'if c.isWhitespace thenfindNextEnd buffer row col.succelselet isKw := isKeyword cconsumeWordToEnd buffer row col isKwpartial def consumeWordToEnd (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0if col.val + 1 >= lineLen then(row, col)elselet lineStr := ViE.getLineFromBuffer buffer row |>.getD ""let nextC := List.getD lineStr.toList (col.val + 1) ' 'let nextKw := isKeyword nextCif nextC.isWhitespace || nextKw != wantKw then(row, col)elseconsumeWordToEnd buffer row col.succ wantKwend
/-- Move to end of word (e) -/def EditorState.moveWordEnd (s : EditorState) : EditorState :=let buffer := s.getActiveBufferlet cursor := s.getCursorlet currLineLen := ViE.getLineLengthFromBuffer buffer cursor.row |>.getD 0let startCol : Col := cursor.col.succlet (r, c) :=if startCol.val >= currLineLen thenif cursor.row.val + 1 < FileBuffer.lineCount buffer thenfindNextEnd buffer cursor.row.succ 0else(cursor.row, ⟨currLineLen⟩)elsefindNextEnd buffer cursor.row startCols.setCursor { row := r, col := c }
let newCol := (getLine s.activeBufferContent prevRow).map String.length |>.getD 0s'.setCursor (Point.make prevRow newCol)
let newLen := ViE.getLineLengthFromBuffer s'.getActiveBuffer prevRow |>.getD 0s'.setCursor { row := prevRow, col := ⟨newLen⟩ }
def EditorState.deleteCharAfterCursor (s : EditorState) : EditorState :=let cursor := s.getCursor-- Check if valid char at cursorlet s' := s.updateActiveBuffer fun buffer =>match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with| some offset =>-- Ensure we don't delete newline if at end of line (unless J behavior, but x usually doesn't join lines)match buffer.table.getLineRange cursor.row.val with| some (_, len) =>if cursor.col.val < len then{ buffer with table := buffer.table.delete offset 1 offsetdirty := true }elsebuffer| none => buffer| none => buffer
def deleteLine (buffer : TextBuffer) (row : Nat) : TextBuffer :=let before := arrayTake buffer rowlet after := arrayDrop buffer (row + 1)if before.isEmpty && after.isEmpty thenemptyTextBuffer -- Minimum one empty line
-- Cursor stays at same position unless it was last charlet newBuffer := s'.getActiveBufferlet newLen := ViE.getLineLengthFromBuffer newBuffer cursor.row |>.getD 0if newLen > 0 && cursor.col.val >= newLen thens'.setCursor { cursor with col := ⟨newLen - 1⟩ }
let newBuffer := s'.activeBufferContentlet newRow := min row (newBuffer.size.pred)let currentLineLen := (getLine newBuffer newRow).map String.length |>.getD 0
let newBuffer := s'.getActiveBufferlet newRowVal := min cursor.row.val (newBuffer.lineCount.pred)let newRow : Row := ⟨newRowVal⟩let currentLineLen := ViE.getLineLengthFromBuffer newBuffer newRow |>.getD 0
def EditorState.deleteRange (s : EditorState) (p1 p2 : Point) : EditorState :=let s' := s.updateActiveBuffer fun buffer =>match buffer.table.getOffsetFromPoint p1.row.val p1.col.val,buffer.table.getOffsetFromPoint p2.row.val p2.col.val with| some off1, some off2 =>let startOff := min off1 off2let endOff := max off1 off2let len := endOff - startOffif len > 0 then{ buffer with table := buffer.table.delete startOff len startOffdirty := true }else buffer| _, _ => buffer-- Move cursor to start of deleted rangelet newStart := if p1.row < p2.row || (p1.row == p2.row && p1.col < p2.col) then p1 else p2let s'' := s'.setCursor newStart{ s'' with inputState := { s''.inputState with previousKey := none } }def EditorState.changeWord (s : EditorState) : EditorState :=let n := if s.getCount == 0 then 1 else s.getCountlet start := s.getCursor-- Apply 'moveWordEnd' n times (recursive helper)let rec applyMotionN (st : EditorState) (count : Nat) : EditorState :=match count with| 0 => st| k + 1 => applyMotionN (st.moveWordEnd) klet endState := applyMotionN s nlet endP := endState.getCursor-- Inclusive deletion logic for 'e' motion behaviorlet buffer := s.getActiveBufferlet lineLen := ViE.getLineLengthFromBuffer buffer endP.row |>.getD 0let targetCol := if endP.col.val + 1 <= lineLen then endP.col.val + 1 else lineLenlet targetP := { endP with col := ⟨targetCol⟩ }
let s' := s.updateActiveBufferContent fun buffer =>let before := arrayTake buffer (cursor.row.val + 1)let after := arrayDrop buffer (cursor.row.val + 1)arrayConcat [before, #[#[]], after]s'.setCursor (Point.make (cursor.row.val + 1) 0)
let s' := s.updateActiveBuffer fun buffer =>match buffer.table.getLineRange cursor.row.val with| some (start, len) =>{ buffer with table := buffer.table.insert (start + len) "\n" (start + len)dirty := true }| none => buffers'.setCursor { row := ⟨cursor.row.val + 1⟩, col := 0 }
let s' := s.updateActiveBufferContent fun buffer =>let before := arrayTake buffer cursor.row.vallet after := arrayDrop buffer cursor.row.valarrayConcat [before, #[#[]], after]s'.setCursor (Point.make cursor.row.val 0)
let s' := s.updateActiveBuffer fun buffer =>match buffer.table.getLineRange cursor.row.val with| some (start, _) =>{ buffer with table := buffer.table.insert start "\n" startdirty := true }| none => buffers'.setCursor { cursor with col := 0 }
let line := getLine s.activeBufferContent cursor.row.val |>.getD ""{ s with clipboard := some #[stringToLine line], message := "Yanked 1 line" }
let line := ViE.getLineFromBuffer s.getActiveBuffer cursor.row |>.getD ""let content := if line.endsWith "\n" then line else line ++ "\n"{ s with clipboard := (some content : Option String), message := "Yanked 1 line" }
let offset := match buffer.table.getOffsetFromPoint (row + 1) 0 with| some off => off| none => buffer.table.tree.length
let (offset, textToInsert) := match buffer.table.getOffsetFromPoint (cursor.row.val + 1) 0 with| some off => (off, text)| none =>let len := buffer.table.tree.lengthif len > 0 then-- Check if buffer ends with newline to avoid merging-- (Optimization: ideally check last char directly)let s_full := buffer.table.toStringif !s_full.endsWith "\n" then(len, "\n" ++ text)else(len, text)else (0, text)
def EditorState.commitEdit (s : EditorState) : EditorState :=s.updateActiveBuffer fun buffer =>{ buffer with table := buffer.table.commit }/-- Vim Operators -/def EditorState.deleteWord (s : EditorState) : EditorState :=let p1 := s.getCursorlet s' := s.moveWordForwardlet p2 := s'.getCursors.deleteRange p1 p2
normal := fun s k => match k with
normal := fun s k =>let handleMotion (state : EditorState) (motion : EditorState → EditorState) : IO EditorState :=let n := if state.getCount == 0 then 1 else state.getCountlet rec applyN (st : EditorState) (count : Nat) : EditorState :=match count with| 0 => st| n + 1 => applyN (motion st) ntermination_by countmatch state.inputState.previousKey with| none => pure $ clearInput (EditorState.clampCursor (applyN state n))| some 'd' =>let start := state.getCursorlet endP := (applyN state n).getCursorpure $ clearInput (state.deleteRange start endP)| some 'c' =>let start := state.getCursorlet endP := (applyN state n).getCursorpure $ clearInput (state.deleteRange start endP |>.setMode Mode.insert)| _ => pure $ clearInput (EditorState.clampCursor (applyN state n))match k with
pure $ clearInput (EditorState.moveCursorLeftN s s.getCount)| Key.char 'j' => pure $ clearInput (EditorState.moveCursorDownN s s.getCount)| Key.char 'k' => pure $ clearInput (EditorState.moveCursorUpN s s.getCount)| Key.char 'l' => pure $ clearInput (EditorState.moveCursorRightN s s.getCount)
handleMotion s EditorState.moveCursorLeft| Key.char 'j' => handleMotion s EditorState.moveCursorDown| Key.char 'k' => handleMotion s EditorState.moveCursorUp| Key.char 'l' => handleMotion s EditorState.moveCursorRight
| Key.char '$' => pure $ clearInput (EditorState.moveToLineEnd s)
| Key.char '$' => handleMotion s EditorState.moveToLineEnd| Key.char 'w' =>match s.inputState.previousKey with| some 'c' => pure $ clearInput (s.changeWord)| _ => handleMotion s EditorState.moveWordForward| Key.char 'b' => handleMotion s EditorState.moveWordBackward| Key.char 'e' => handleMotion s EditorState.moveWordEnd| Key.char 'x' => pure $ clearInput (EditorState.deleteCharAfterCursor s)
| 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' } }
match s.inputState.previousKey with| some 'g' =>-- gg implementationlet n := s.getCountlet line := if n > 0 then n else 1pure $ clearInput (EditorState.jumpToLine s line)| _ => pure { s with inputState := { s.inputState with previousKey := some 'g' } }
pure { s with inputState := { s.inputState with previousKey := some 'g' } }
-- This case is only reached if we pushed a char and pending became exactly "\x1b",-- which is impossible if start condition was "pending.length > 0" (meaning pending was already "\x1b")-- UNLESS previous pending was empty? No, then it goes to else block.-- Wait, if pending was "\x1b" and we pushed nothing? No, we always push c.-- So this case is indeed impossible for Escape+Char.
def modifyLineInBuffer (buffer : FileBuffer) (row : Nat) (f : String → String) : FileBuffer :=match buffer.table.getLineRange row with
def modifyLineInBuffer (buffer : FileBuffer) (row : Row) (f : String → String) : FileBuffer :=match buffer.table.getLineRange row.val with
def getLine (buffer : TextBuffer) (n : Nat) : Option String :=if h : n < buffer.size thensome (lineToString buffer[n])
def getLine (buffer : TextBuffer) (n : Row) : Option String :=if h : n.val < buffer.size thensome (lineToString buffer[n.val])
def modifyLine (buffer : TextBuffer) (row : Nat) (f : String → String) : TextBuffer :=if h : row < buffer.size thenlet oldLine := buffer[row]
def modifyLine (buffer : TextBuffer) (row : Row) (f : String → String) : TextBuffer :=if h : row.val < buffer.size thenlet oldLine := buffer[row.val]
import ViE.State.Configimport ViE.Configimport ViE.Command.Implimport ViE.Key.Mapimport ViE.State.Editimport ViE.State.Movementnamespace Test.Modeopen ViEdef assert (msg : String) (cond : Bool) : IO Unit := doif cond thenIO.println s!"[PASS] {msg}"elseIO.println s!"[FAIL] {msg}"throw (IO.userError s!"Assertion failed: {msg}")-- Helper to construct a full Configdef makeTestConfig : Config := {settings := ViE.defaultConfigcommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}-- Run a sequence of keysdef runKeys (startState : EditorState) (keys : List Key) : IO EditorState := dolet config := makeTestConfiglet mut s := startStatefor k in keys dos ← ViE.update config s kreturn sdef test : IO Unit := doIO.println "Starting Mode Test..."let s := ViE.initialState-- Scenario: Insert 'abc' then Esc.-- Initial: (0,0)-- 'i' -> Insert Mode-- 'a' -> "a", (0,1)-- 'b' -> "ab", (0,2)-- 'c' -> "abc", (0,3)-- Esc -> Normal Mode.-- Expected Vim behavior: Cursor should move left to (0,2) 'c'.-- If empty line "insert a then esc", "a" (0,1) -> (0,0).let keys := [Key.char 'i', Key.char 'a', Key.char 'b', Key.char 'c', Key.esc]let sEnd ← runKeys s keys-- Check Modeif sEnd.mode != Mode.normal thenIO.println s!"[FAIL] Mode mismatch. Expected Normal, got {sEnd.mode}"assert "Mode is Normal" falseelseIO.println "[PASS] Mode is Normal"-- Check Textlet text := getLineFromBuffer sEnd.getActiveBuffer 0 |>.getD ""if text != "abc" thenIO.println s!"[FAIL] Text mismatch. Expected 'abc', got '{text}'"assert "Text is 'abc'" falseelseIO.println "[PASS] Text is 'abc'"-- Check Cursor-- Expect (0, 2)let cursor := sEnd.getCursorif cursor.col.val != 2 thenIO.println s!"[FAIL] Cursor mismatch. Expected (0, 2), got ({cursor.row.val}, {cursor.col.val})"assert "Cursor moved left on Esc" falseelseIO.println "[PASS] Cursor moved left on Esc"IO.println "ModeTest passed!"end Test.Mode
import ViE.State.Movementimport ViE.State.Editimport ViE.Key.Mapimport ViE.Typesimport ViE.Buffer.Contentimport ViE.Configimport ViE.Command.Implnamespace Test.Keybindsopen ViEdef makeTestConfig : Config := {settings := ViE.defaultConfigcommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}def keys (s : String) : List Key :=s.toList.map fun c =>if c == '\n' then Key.enter else Key.char cdef runKeys (s : EditorState) (ks : List Key) : IO EditorState := dolet config := makeTestConfigks.foldlM (fun s k => ViE.update config s k) sdef assert (msg : String) (cond : Bool) : IO Unit := doif !cond thenthrow (IO.userError s!"Assertion failed: {msg}")def testMotions : IO Unit := doIO.println " Testing Motions..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "line1\nline2\nline3" ++ [Key.esc] ++ keys "gg0")-- "line1\nline2\nline3" cursor at (0,0)-- l, hlet s_l ← runKeys s1 [Key.char 'l']if s_l.getCursor != Point.make 0 1 thenlet c := s_l.getCursorlet line := ViE.getLineFromBuffer s_l.getActiveBuffer c.row |>.getD "ERR"let len := ViE.getLineLengthFromBuffer s_l.getActiveBuffer c.row |>.getD 999IO.println s!"DEBUG FAILURE: l motion. Cursor: ({c.row.val}, {c.col.val}). Line 0: '{line}' (len: {len})"assert "l moves right" (s_l.getCursor == Point.make 0 1)let s_lh ← runKeys s_l [Key.char 'h']assert "h moves left" (s_lh.getCursor == Point.make 0 0)-- j, klet s_j ← runKeys s1 [Key.char 'j']assert "j moves down" (s_j.getCursor == Point.make 1 0)let s_jk ← runKeys s_j [Key.char 'k']assert "k moves up" (s_jk.getCursor == Point.make 0 0)-- 0, $-- 0, $let s_end ← runKeys s1 [Key.char '$']assert "$ moves to end" (s_end.getCursor == Point.make 0 4) -- '1' is at col 4let s_start ← runKeys s_end [Key.char '0']assert "0 moves to start" (s_start.getCursor == Point.make 0 0)-- w, b, elet s_text ← runKeys s0 ([Key.char 'i'] ++ keys "word1 word2" ++ [Key.esc] ++ [Key.char '0'])let s_w ← runKeys s_text [Key.char 'w']assert "w moves to next word" (s_w.getCursor == Point.make 0 6)let s_e ← runKeys s_text [Key.char 'e']assert "e moves to end of word" (s_e.getCursor == Point.make 0 4)let s_we ← runKeys s_w [Key.char 'e']assert "we moves to end of next word" (s_we.getCursor == Point.make 0 10)let s_web ← runKeys s_we [Key.char 'b']assert "b moves to start of word" (s_web.getCursor == Point.make 0 6)-- gg, Glet s_G ← runKeys s1 [Key.char 'G']assert "G moves to last line" (s_G.getCursor.row == 2)let s_gg ← runKeys s_G [Key.char 'g', Key.char 'g']assert "gg moves to first line" (s_gg.getCursor.row == 0)-- | (jump to column)let s_pipe ← runKeys s1 [Key.char '3', Key.char '|']assert "| jumps to column" (s_pipe.getCursor.col == 2) -- 1-indexed count 3 -> col 2def testEditing : IO Unit := doIO.println " Testing Editing..."let s0 := ViE.initialState-- i, a, Alet s_i ← runKeys s0 [Key.char 'i', Key.char 'x', Key.esc]assert "i inserts" (s_i.getActiveBuffer.table.toString == "x")let s_a ← runKeys s_i [Key.char 'a', Key.char 'y', Key.esc]assert "a appends" (s_a.getActiveBuffer.table.toString == "xy")let s_A ← runKeys s_a [Key.char '0', Key.char 'A', Key.char 'z', Key.esc]assert "A appends at end" (s_A.getActiveBuffer.table.toString == "xyz")-- o, Olet s_o ← runKeys s_i [Key.char 'o', Key.char 'y', Key.esc]assert "o inserts line below" (s_o.getActiveBuffer.table.toString == "x\ny")let s_O ← runKeys s_o [Key.char 'k', Key.char 'O', Key.char 'z', Key.esc]assert "O inserts line above" (s_O.getActiveBuffer.table.toString == "z\nx\ny")-- xlet s_x ← runKeys s_i [Key.char 'x']assert "x deletes char" (s_x.getActiveBuffer.table.toString == "")def testOperators : IO Unit := doIO.println " Testing Operators..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "hello world" ++ [Key.esc] ++ [Key.char '0'])-- dwlet s_dw ← runKeys s1 [Key.char 'd', Key.char 'w']assert "dw deletes word" (s_dw.getActiveBuffer.table.toString == "world")-- cwlet s_cw ← runKeys s1 [Key.char 'c', Key.char 'w', Key.char 'h', Key.char 'i', Key.esc]assert "cw changes word" (s_cw.getActiveBuffer.table.toString == "hi world")-- ddlet s_lines ← runKeys s0 ([Key.char 'i'] ++ keys "line1\nline2\nline3" ++ [Key.esc] ++ keys "ggj")let s_dd ← runKeys s_lines [Key.char 'd', Key.char 'd']assert "dd deletes current line" (s_dd.getActiveBuffer.table.toString == "line1\nline3")-- yy, p, Plet s_yy ← runKeys s_lines [Key.char 'g', Key.char 'g', Key.char 'y', Key.char 'y']let s_p ← runKeys s_yy [Key.char 'G', Key.char 'p']let p_res := s_p.getActiveBuffer.table.toStringif p_res != "line1\nline2\nline3\nline1\n" thenIO.println s!"DEBUG FAILURE: p paste. Expected 'line1\\nline2\\nline3\\nline1\\n', got '{p_res}'"assert "p pastes below" (s_p.getActiveBuffer.table.toString == "line1\nline2\nline3\nline1\n")let s_P ← runKeys s_yy [Key.char 'g', Key.char 'g', Key.char 'P']assert "P pastes above" (s_P.getActiveBuffer.table.toString == "line1\nline1\nline2\nline3")def testVisual : IO Unit := doIO.println " Testing Visual Mode..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "highlight me" ++ [Key.esc] ++ [Key.char '0'])-- v, dlet s_v ← runKeys s1 [Key.char 'v', Key.char 'l', Key.char 'd']assert "visual d deletes selection" (s_v.getActiveBuffer.table.toString == "ghlight me")-- v, y, plet s_vy ← runKeys s1 [Key.char 'v', Key.char 'e', Key.char 'y']let s_vyp ← runKeys s_vy [Key.char '$', Key.char 'p']assert "visual y yanks selection" (s_vyp.getActiveBuffer.table.toString == "highlight me\nhighlight")def testCounted : IO Unit := doIO.println " Testing Counted Actions..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "a b c d e" ++ [Key.esc] ++ [Key.char '0'])-- 3wlet s_3w ← runKeys s1 [Key.char '3', Key.char 'w']assert "3w moves 3 words" (s_3w.getCursor.col == 6) -- positions of 'a', 'b', 'c', 'd' start: 0, 2, 4, 6-- 2ddlet s_lines ← runKeys s0 ([Key.char 'i'] ++ keys "1\n2\n3\n4" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g'])-- Not all counted actions might be implemented yet, check Map.lean-- Map.lean uses s.getCount for h,j,k,l. dd uses previousKey, doesn't seem to use count yet.-- Let's test what is implemented.-- 2jlet s_2j ← runKeys s_lines [Key.char '2', Key.char 'j']assert "2j moves 2 lines down" (s_2j.getCursor.row == 2)def test : IO Unit := doIO.println "Starting Expanded Keybind Tests..."testMotionstestEditingtestOperatorstestVisualtestCountedIO.println "All Expanded Keybind Tests passed!"end Test.Keybinds
assert s!"Cursor after insert 'd' should be (0,1) but is ({c3.row.val}, {c3.col.val})" (c3.row.val == 0 && c3.col.val == 1)
assert s!"Cursor after insert 'd' and Esc should be (0,0) but is ({c3.row.val}, {c3.col.val})" (c3.row.val == 0 && c3.col.val == 0)
import ViE.State.Configimport ViE.Configimport ViE.Command.Implimport ViE.Key.Mapimport ViE.State.Editnamespace Test.BugReproductionopen ViEdef assert (msg : String) (cond : Bool) : IO Unit := doif cond thenIO.println s!"[PASS] {msg}"elseIO.println s!"[FAIL] {msg}"throw (IO.userError s!"Assertion failed: {msg}")-- Helper to construct a full Configdef makeTestConfig : Config := {settings := ViE.defaultConfigcommands := ViE.Command.defaultCommandMapbindings := ViE.Key.makeKeyMap ViE.Command.defaultCommandMap}-- Run a sequence of keysdef runKeys (startState : EditorState) (keys : List Key) : IO EditorState := dolet config := makeTestConfiglet mut s := startStatefor k in keys dos ← ViE.update config s kreturn sdef test : IO Unit := doIO.println "Starting Bug Reproduction Test..."let s := ViE.initialState-- Scenario: Insert, Undo, Insertlet s1 := s.insertChar 'a'let s1 := s1.commitEdit -- Force separate undo grouplet s2 := s1.insertChar 'b'-- Text: 'ab', Cursor: (0, 2)let s3 := s2.undo-- Text: 'a', Cursor should be (0, 1)let cursor := s3.getCursorif cursor.col.val != 1 thenIO.println s!"[FAIL] Undo cursor mismatch. Expected 1, got {cursor.col.val}"assert "Undo cursor" falseelseIO.println "[PASS] Undo cursor correct"let s4 := s3.insertChar 'c'-- Text: 'ac'let text := getLineFromBuffer s4.getActiveBuffer 0 |>.getD ""if text != "ac" thenIO.println s!"[FAIL] Insert after undo failed. Expected 'ac', got '{text}'"assert "Insert after undo" falseelseIO.println "[PASS] Insert after undo works"-- Scenario: Paste, Undo, Paste (checking grouping too, but focusing on cursor)-- Resetlet s := ViE.initialStatelet s := s.insertChar 'x'let s := s.yankCurrentLine -- Yank 'x\n'let s := s.pasteBelow -- Paste 'x\n' -> 'x\nx\n' ??-- PasteBelow pastes line.-- Scenario: x commandlet s := ViE.initialStatelet s := s.insertChar 'h'let s := s.insertChar 'e'let s := s.insertChar 'y'-- "hey"let s := (s.moveCursorLeft).moveCursorLeft -- At 'h' (0,0)? No: 3 -> 2 -> 1. 'e'-- "hey" cursor at 2 ('y'). Left -> 1 ('e'). Left -> 0 ('h').-- Actually moveCursorLeft from (0,3) -> (0,2) 'y'.-- Let's use setCursorlet s := s.setCursor (Point.make 0 1) -- 'e'let s := s.deleteCharAfterCursor -- Should delete 'e' -> "hy"let text := getLineFromBuffer s.getActiveBuffer 0 |>.getD ""if text != "hy" thenIO.println s!"[FAIL] 'x' command (deleteCharAfterCursor) failed. Expected 'hy', got '{text}'"assert "x command" falseelseIO.println "[PASS] 'x' command works"IO.println "Bug Reproduction Test Finished"end Test.BugReproduction