5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC [[lean_exe]]name = "test"root = "Test"
modifyLineInBuffer buffer row fun line =>let chars := line.toListlet newChars := (chars.take col) ++ [c] ++ (chars.drop col)String.ofList newChars
match buffer.table.getOffsetFromPoint row col with| some offset => { buffer with table := buffer.table.insert offset (c.toString) offsetdirty := true }| none => buffer
let s' := s.updateActiveBufferContent fun buffer =>let beforeLines := arrayTake buffer rowlet afterLines := arrayDrop buffer (row + 1)arrayConcat [beforeLines, #[stringToLine beforeSplit, stringToLine afterSplit], afterLines]
-- Use direct PieceTable insert for atomic undolet s' := s.updateActiveBuffer fun buffer =>match buffer.table.getOffsetFromPoint row col with| some offset => { buffer with table := buffer.table.insert offset "\n" offsetdirty := true }| none => buffer
let s' := s.updateActiveBufferContent fun buffer =>modifyLine buffer row fun line =>let chars := line.toListlet newChars := (chars.take (col - 1)) ++ (chars.drop col)String.ofList newChars
let s' := s.updateActiveBuffer fun buffer =>match buffer.table.getOffsetFromPoint row (col - 1) with| some offset =>{ buffer with table := buffer.table.delete offset 1 (offset + 1)dirty := true }| none => buffer
let s' := s.updateActiveBufferContent fun buffer =>let beforeLines := arrayTake buffer prevRowlet afterLines := arrayDrop buffer (row + 1)arrayConcat [beforeLines, #[stringToLine mergedLine], afterLines]
let s' := s.updateActiveBuffer fun buffer =>-- Verify we are deleting the newline at the end of prevRow.match buffer.table.getLineRange prevRow with| some (start, len) =>-- Newline is at start + len. Length of newline is 1 (for \n).-- Check EOL consistency?-- cursor for undo should be at start+len (before newline){ buffer with table := buffer.table.delete (start + len) 1 (start + len)dirty := true }| none => buffer
let s' := s.updateActiveBufferContent fun (buffer : TextBuffer) => deleteLine buffer cursor.row.val
let row := cursor.row.vallet s' := s.updateActiveBuffer fun buffer =>match buffer.table.getLineRange row with| some (start, len) =>let deleteLen := if row < FileBuffer.lineCount buffer - 1 then len + 1 else len-- Restore cursor at start of line{ buffer with table := buffer.table.delete start deleteLen startdirty := true }| none => buffer-- Reset cursor logic
let s' := s.updateActiveBufferContent fun buffer =>let before := arrayTake buffer (cursor.row.val + 1)let after := arrayDrop buffer (cursor.row.val + 1)arrayConcat [before, lines, after]s'.setCursor (Point.make (cursor.row.val + lines.size) 0)
let row := cursor.row.val-- Convert lines to string block (linewise paste)let text := String.intercalate "\n" (lines.toList.map fun l => String.ofList l.toList) ++ "\n"let s' := s.updateActiveBuffer fun buffer =>-- Determine insert offset.-- Try start of next line. If EOF, append.let offset := match buffer.table.getOffsetFromPoint (row + 1) 0 with| some off => off| none => buffer.table.tree.length-- For paste, undo should restore cursor to insertion point-- Break undo grouping to ensure separate paste operations are distinctlet pt := buffer.table.commit{ buffer with table := pt.insert offset text offsetdirty := true }s'.setCursor (Point.make (row + 1) 0)
let s' := s.updateActiveBufferContent fun buffer =>let before := arrayTake buffer cursor.row.vallet after := arrayDrop buffer cursor.row.valarrayConcat [before, lines, after]s'.setCursor (Point.make cursor.row.val 0)
let row := cursor.row.vallet text := String.intercalate "\n" (lines.toList.map fun l => String.ofList l.toList) ++ "\n"let s' := s.updateActiveBuffer fun buffer =>let offset := match buffer.table.getOffsetFromPoint row 0 with| some off => off| none => 0let pt := buffer.table.commit{ buffer with table := pt.insert offset text offsetdirty := true }s'.setCursor (Point.make row 0)def EditorState.undo (s : EditorState) : EditorState :=-- Capture current cursor offset (if valid) for redolet buf := s.getActiveBufferlet currentOffset := match buf.table.getOffsetFromPoint s.getCursor.row.val s.getCursor.col.val with| some off => off| none => 0
let (newTable, cursorOpt) := buf.table.undo currentOffsetlet s' := s.updateActiveBuffer fun _ => { buf with table := newTable, dirty := true }match cursorOpt with| some off =>let (r, c) := newTable.getPointFromOffset offlet s'' := s'.setCursor (Point.make r c){ s'' with message := "Undo" }| none => { s' with message := "Already at oldest change" }def EditorState.redo (s : EditorState) : EditorState :=-- Capture current cursor offsetlet buf := s.getActiveBufferlet currentOffset := match buf.table.getOffsetFromPoint s.getCursor.row.val s.getCursor.col.val with| some off => off| none => 0let (newTable, cursorOpt) := buf.table.redo currentOffsetlet s' := s.updateActiveBuffer fun _ => { buf with table := newTable, dirty := true }match cursorOpt with| some off =>let (r, c) := newTable.getPointFromOffset offlet s'' := s'.setCursor (Point.make r c){ s'' with message := "Redo" }| none => { s' with message := "Already at newest change" }
{ pt' with tree := newTree }
-- Check optimization/merge compatibilitylet (finalUndoStack, newLastInsert) :=match pt.lastInsert with| some (lastOff, lastAddOff) =>if offset == lastOff && lastAddOff == pt.add.size then-- MERGE: Contiguous edit in doc and add buffer.-- Don't push to undoStack (reuse previous state as undo point)(pt.undoStack, some (offset + text.utf8ByteSize, lastAddOff + text.utf8ByteSize))else-- NO MERGE: Push current statelet stack := (pt.tree, cursorOffset) :: pt.undoStacklet params := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack(params, some (offset + text.utf8ByteSize, pt.add.size + text.utf8ByteSize))| none =>let stack := (pt.tree, cursorOffset) :: pt.undoStacklet params := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack(params, some (offset + text.utf8ByteSize, pt.add.size + text.utf8ByteSize)){ pt' withtree := newTreeundoStack := finalUndoStackredoStack := []lastInsert := newLastInsert}
{ pt with tree := newTree }
let stack := (pt.tree, cursorOffset) :: pt.undoStacklet finalStack := if stack.length > pt.undoLimit then stack.take pt.undoLimit else stack{ pt withtree := newTreeundoStack := finalStackredoStack := []lastInsert := none -- Break merge chain}/-- Commit the current edit group, forcing the next insert to start a new undo item. -/def PieceTable.commit (pt : PieceTable) : PieceTable :={ pt with lastInsert := none }/-- Undo the last operation -/def PieceTable.undo (pt : PieceTable) (currentCursor : Nat) : PieceTable × Option Nat :=match pt.undoStack with| [] => (pt, none)| (prev, prevCursor) :: rest =>({ pt withtree := prevundoStack := restredoStack := (pt.tree, currentCursor) :: pt.redoStacklastInsert := none}, some prevCursor)/-- Redo the last undone operation -/def PieceTable.redo (pt : PieceTable) (currentCursor : Nat) : PieceTable × Option Nat :=match pt.redoStack with| [] => (pt, none)| (next, nextCursor) :: rest =>({ pt withtree := nextundoStack := (pt.tree, currentCursor) :: pt.undoStackredoStack := restlastInsert := none}, some nextCursor)
/-- Get byte offset from Row/Col position -/def PieceTable.getOffsetFromPoint (pt : PieceTable) (row col : Nat) : Option Nat :=match PieceTable.getLineRange pt row with| some (startOff, len) =>-- Allow col up to len (inclusive) for appending at end of lineif col <= len then some (startOff + col)else if col == len + 1 then some (startOff + len) -- Lenient for cursor logic? No, strict.else some (startOff + len) -- Clamp to end of line if strictly greater? Better to be safe.| none => none
def PieceTable.lineCount (pt : PieceTable) : Nat :=match pt.tree with| .leaf _ s => s.lines + 1| .internal _ s => s.lines + 1| .empty => 1partial def PieceTable.findLineForOffset (pt : PieceTable) (target : Nat) (low high : Nat) : Option (Nat × Nat) :=if low > high then noneelselet mid := (low + high) / 2match pt.getLineRange mid with| some (start, len) =>let endOff := start + lenif target >= start && target <= endOff thensome (mid, target - start)else if target < start thenif mid == 0 then noneelse PieceTable.findLineForOffset pt target low (mid - 1)elsePieceTable.findLineForOffset pt target (mid + 1) high| none => nonedef PieceTable.getPointFromOffset (pt : PieceTable) (offset : Nat) : (Nat × Nat) :=match PieceTable.findLineForOffset pt offset 0 pt.lineCount with| some (r, c) => (r, c)| none => (0, 0) -- Fallback
import Test.Undoimport Test.Bufferimport Test.Layoutimport Test.Integrationdef main : IO Unit := doIO.println "Running all tests..."Test.Undo.testTest.Buffer.testTest.Layout.testTest.Integration.testIO.println "All tests finished."
import ViE.Data.PieceTableopen ViE.PieceTablenamespace Test.Undodef 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}")def test : IO Unit := doIO.println "Starting Undo/Redo Test..."-- 1. Create initial bufferlet initialText := "Hello, World!"let pt0 := PieceTable.fromString initialTextassert "Initial text correct" (pt0.toString == initialText)assert "Initial undo stack empty" (pt0.undoStack.isEmpty)-- 2. Insert " New" at end-- "Hello, World! New"let pt1 := pt0.insert 13 " New" 13assert "Text after insert" (pt1.toString == "Hello, World! New")assert "Undo stack has 1 item" (pt1.undoStack.length == 1)-- 3. Delete ", World"-- "Hello! New"-- "Hello, World!" -> offset 5, delete 7 (", World")let pt2 := pt1.delete 5 7 5assert "Text after delete" (pt2.toString == "Hello! New")assert "Undo stack has 2 items" (pt2.undoStack.length == 2)-- 4. Undo Modify (Delete)-- Should revert to "Hello, World! New"let (pt3, _) := pt2.undo 0assert "Text after undo delete" (pt3.toString == "Hello, World! New")assert "Undo stack has 1 item" (pt3.undoStack.length == 1)assert "Redo stack has 1 item" (pt3.redoStack.length == 1)-- 5. Undo Insert-- Should revert to "Hello, World!"let (pt4, _) := pt3.undo 0assert "Text after undo insert" (pt4.toString == "Hello, World!")assert "Undo stack has 0 items" (pt4.undoStack.isEmpty)assert "Redo stack has 2 items" (pt4.redoStack.length == 2)-- 6. Redo Insert-- Should go to "Hello, World! New"let (pt5, _) := pt4.redo 0assert "Text after redo insert" (pt5.toString == "Hello, World! New")assert "Undo stack has 1 item" (pt5.undoStack.length == 1)assert "Redo stack has 1 item" (pt5.redoStack.length == 1)-- 7. Redo Delete-- Should go to "Hello! New"let (pt6, _) := pt5.redo 0assert "Text after redo delete" (pt6.toString == "Hello! New")assert "Undo stack has 2 items" (pt6.undoStack.length == 2)assert "Redo stack empty" (pt6.redoStack.isEmpty)-- 8. Test Redo clearing on new editlet (pt7, _) := pt6.undo 0 -- "Hello, World! New"-- Insert " Again" at end -> "Hello, World! New Again"let pt8 := pt7.insert 17 " Again" 17assert "Text after new insert" (pt8.toString == "Hello, World! New Again")assert "Redo stack cleared" (pt8.redoStack.isEmpty)-- 9. Test Optimization (Grouping)-- Force break merge chain from previous step to ensure " 1" starts a new grouplet pt8_clean := { pt8 with lastInsert := none }let pt9 := pt8_clean.insert 23 " 1" 23 -- "Hello, World! New Again 1"let pt10 := pt9.insert 25 "2" 25 -- "Hello, World! New Again 12"let pt11 := pt10.insert 26 "3" 26 -- "Hello, World! New Again 123"assert "Text after group insert" (pt11.toString == "Hello, World! New Again 123")-- Should have only 1 new undo item for " 123" because they overlap-- pt8 had some undo stack. pt9 added 1. pt10 merged. pt11 merged.-- So pt11.undoStack.length should be pt8.undoStack.length + 1assert "Undo stack grouped" (pt11.undoStack.length == pt8.undoStack.length + 1)let (pt12, _) := pt11.undo 0assert "Undo removes group" (pt12.toString == "Hello, World! New Again")-- 10. Test Limit-- Force a small limitlet ptLimit := { pt12 with undoLimit := 2 }let ptL1 := (ptLimit.insert 0 "A" 0) -- Stack: 1let ptL2 := (ptL1.insert 0 "B" 0) -- Stack: 2-- Previous insert was "A" at 0. LastInsert = (0 + 1, addOffset + 1).-- Current insert at 0. 0 != 1. So NOT contiguous. Correct.let ptL3 := (ptL2.insert 0 "C" 0) -- Stack: 3 -> capped to 2assert "Undo limit respected" (ptL3.undoStack.length == 2)-- The oldest undo (for "A") should be dropped. The remaining undos are "C" -> "B", and "B" -> "A".-- So undoing twice should start with "CBA..." -> "BA..." -> "A..."let (u1, _) := ptL3.undo 0let (u2, _) := u1.undo 0assert "Oldest undo dropped" (u2.toString == "AHello, World! New Again")assert "Oldest undo dropped" (u2.toString == "AHello, World! New Again")-- 11. Test Paste Undo Grouping (Reproduction)-- Scenario: Paste "P1" then Paste "P2". They should NOT merge if we signal a break,-- OR if we consider pastes as distinct operations that shouldn't auto-merge like typing.-- Currently PieceTable merges ANY contiguous insert.let ptBase := PieceTable.fromString ""let ptP1 := ptBase.insert 0 "P1" 0 -- Simulate Paste 1-- Simulate EditorState.paste calling commit before next insertlet ptP1_committed := ptP1.commitlet ptP2 := ptP1_committed.insert 2 "P2" 2 -- Simulate Paste 2 (contiguous)assert "Text is P1P2" (ptP2.toString == "P1P2")-- Expectation: 2 undo items (one for P1, one for P2).-- Bug: they merge into 1 item because offset 2 == lastInsert end.if ptP2.undoStack.length == 1 thenIO.println "[FAIL] Paste operations merged (expected 2 undo items)"assert "Paste should not merge" falseelseIO.println "[PASS] Paste operations distinct (2 undo items)"IO.println "TestUndo passed!"end Test.Undo
import ViE.Typesopen ViEnamespace Test.Layoutdef 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}")def test : IO Unit := doIO.println "Starting Layout Test..."-- 1. Construct Layoutslet view1 : ViewState := { bufferId := 1, cursor := {row:=0, col:=0}, scrollRow:=0, scrollCol:=0 }let win1 := Layout.window 1 view1let view2 : ViewState := { bufferId := 2, cursor := {row:=0, col:=0}, scrollRow:=0, scrollCol:=0 }let win2 := Layout.window 2 view2-- 2. Test Split Constructionlet hsplit := Layout.hsplit win1 win2 0.5match hsplit with| .hsplit l r ratio =>assert "HSplit match" trueassert "HSplit ratio" (ratio == 0.5)| _ => assert "HSplit construction failed" falselet vsplit := Layout.vsplit hsplit win1 0.3match vsplit with| .vsplit t b ratio =>assert "VSplit match" trueassert "VSplit ratio" (ratio == 0.3)match t with| .hsplit _ _ _ => assert "VSplit top is HSplit" true| _ => assert "VSplit top incorrect" false| _ => assert "VSplit construction failed" falseIO.println "LayoutTest passed!"end Test.Layout
import ViE.Typesimport ViE.State.Configimport ViE.Configimport ViE.Key.Mapimport ViE.Command.Implopen ViEnamespace Test.Integrationdef 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 s-- Helper: Convert string to list of char keysdef keys (s : String) : List Key :=s.toList.map Key.chardef test : IO Unit := doIO.println "Starting Integration Test..."-- Test 1: Typing "abc" -> Undo -> Insert "d"-- Expected: "abc" -> "" -> "d"-- Bug Report: After Undo, Insert mode might fail or buffer might be corruptedlet s0 := ViE.initialState-- 1. Insert "abc"-- i a b c Esclet input1 := [Key.char 'i'] ++ keys "abc" ++ [Key.esc]let s1 ← runKeys s0 input1let text1 := (s1.getActiveBuffer.table.toString)assert "Text after insert abc" (text1 == "abc")-- 2. Undo-- ulet s2 ← runKeys s1 [Key.char 'u']let text2 := (s2.getActiveBuffer.table.toString)assert "Text after undo" (text2 == "")-- Cursor check: Should be back at (0, 0)let c2 := s2.getCursorassert s!"Cursor after undo should be (0,0) but is ({c2.row.val}, {c2.col.val})" (c2.row.val == 0 && c2.col.val == 0)-- 3. Insert "d"-- i d Esclet s3 ← runKeys s2 [Key.char 'i', Key.char 'd', Key.esc]let text3 := (s3.getActiveBuffer.table.toString)assert "Text after re-insert d" (text3 == "d")let c3 := s3.getCursorassert 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)IO.println "IntegrationTest passed!"end Test.Integration
import ViE.Buffer.Contentimport ViE.Typesimport ViE.Data.PieceTableopen ViEopen ViE.PieceTablenamespace Test.Bufferdef 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}")def test : IO Unit := doIO.println "Starting Buffer Test..."-- 1. Test fromString and getLinelet text := "Hello\nWorld"let pt := PieceTable.fromString textlet buf : FileBuffer := { initialFileBuffer with table := pt }-- Check linesmatch getLineFromBuffer buf 0 with| some l => assert "Line 0 is Hello" (l == "Hello")| none => assert "Line 0 missing" falsematch getLineFromBuffer buf 1 with| some l => assert "Line 1 is World" (l == "World")| none => assert "Line 1 missing" falsematch getLineFromBuffer buf 2 with| some _ => assert "Line 2 should be missing" false| none => assert "Line 2 correctly missing" true-- 2. Test FileBuffer <-> TextBuffer conversionlet tb : TextBuffer := #[ #['A', 'B'], #['C'] ] -- "AB\nC"let buf2 := ViE.Buffer.fileBufferFromTextBuffer 1 (some "test.txt") tbassert "Buffer created from TextBuffer id" (buf2.id == 1)assert "Buffer created from TextBuffer filename" (buf2.filename == some "test.txt")let tb2 := ViE.Buffer.fileBufferToTextBuffer buf2assert "Roundtrip TextBuffer size" (tb2.size == 2)if tb2.size == 2 thenlet l0 := tb2[0]!let l1 := tb2[1]!assert "Roundtrip Line 0" (String.ofList l0.toList == "AB")assert "Roundtrip Line 1" (String.ofList l1.toList == "C")IO.println "BufferTest passed!"end Test.Buffer