CNJGJCJZ6LRHHIRSRATSE3D3Z5OQGSSTDMXCPVXSKRQLYJFME6IAC YILSJ2SNU6DNZVSFL4MD6QSNLQHUNSBSTGGEQCFTWFTRR62IXBWAC NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC 6W6OJAUT3KLOXXKYR4GA3MG4ACLO2T4KX3SGD2KZDX6MYEZYTPHAC U45XPF3YKPXXRJ4MN24T2RV7GOL4FZKQSWX5P5I7WT4HC5XF4FHAC WRBKZMYVNHRWT7TTUGTDJ3TMWZB32QYW5PCLKTTVAJ2YF6OI3LTAC 5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC XCVPXP4UBFU25NF6VQC3MEYHHH45RL2UXM5TA6O23NA64FPCCCJQC GUD2J453E3UTRJZIEEUUJ3ZIGL72ETUXTO57XQIZ2Y3ZU3C2R55QC DTAIE7PK6TZLNSBQGENS6RT7FFOTMAPSE6ZTPDADINGJF5NTHLWQC /-- Find all occurrences of a byte pattern within a byte array. -/partial def findAllMatchesBytes (haystack : ByteArray) (needle : ByteArray) : Array (Nat × Nat) :=let n := needle.sizelet h := haystack.sizeif n == 0 || h < n then#[]elselet rec matchesAt (i j : Nat) : Bool :=if j == n then trueelse if haystack[i + j]! == needle[j]! then matchesAt i (j + 1) else falselet rec loop (i : Nat) (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=if i + n > h then accelselet acc' := if matchesAt i 0 then acc.push (i, i + n) else accloop (i + 1) acc'loop 0 #[]def updateSearchLineCache (st : EditorState) (lineIdx : Row) (lineStr : String) (matchRanges : Array (Nat × Nat)) : EditorState :=match st.searchState with| none => st| some ss =>let lineMatches := ss.lineMatches.insert lineIdx (lineStr, matchRanges)let order :=if ss.lineOrder.contains lineIdx thenss.lineOrderelsess.lineOrder.push lineIdxlet (lineMatches, order) :=if order.size > ss.lineCacheMax thenlet dropCount := order.size - ss.lineCacheMaxlet evicted := order.extract 0 dropCountlet order := order.extract dropCount order.sizelet lineMatches := evicted.foldl (fun acc r => acc.erase r) lineMatches(lineMatches, order)else(lineMatches, order){ st with searchState := some { ss with lineMatches := lineMatches, lineOrder := order } }
let prefetchSearchMatches (st : EditorState) (buf : FileBuffer) (startRow endRow : Nat) : EditorState :=match st.searchState with| none => st| some ss =>if ss.pattern.isEmpty thenstelselet totalLines := FileBuffer.lineCount buflet rec loop (row : Nat) (acc : EditorState) : EditorState :=if row >= endRow thenaccelse if row >= totalLines thenaccelselet 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 thenloop (row + 1) accelselet matchRanges := findAllMatchesBytes lineStr.toUTF8 ss2.pattern.toUTF8let acc' := updateSearchLineCache acc lineIdx lineStr matchRangesloop (row + 1) acc'| none =>let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss2.pattern.toUTF8let acc' := updateSearchLineCache acc lineIdx lineStr matchRangesloop (row + 1) acc'loop startRow st
let prefetchMargin := 20let totalLines := FileBuffer.lineCount buflet startRow := if view.scrollRow.val > prefetchMargin then view.scrollRow.val - prefetchMargin else 0let endRow := min totalLines (view.scrollRow.val + workH + prefetchMargin)currentSt := prefetchSearchMatches currentSt buf startRow endRow
let (searchMatches, searchSt) :=match st.searchState with| some ss =>if ss.pattern.isEmpty then(#[], currentSt)elsematch ss.lineMatches.find? lineIdx with| some (cachedLine, cachedMatches) =>if cachedLine == lineStr then(cachedMatches, currentSt)elselet matchRanges := findAllMatchesBytes lineStr.toUTF8 ss.pattern.toUTF8let st' := updateSearchLineCache currentSt lineIdx lineStr matchRanges(matchRanges, st')| none =>let matchRanges := findAllMatchesBytes lineStr.toUTF8 ss.pattern.toUTF8let st' := updateSearchLineCache currentSt lineIdx lineStr matchRanges(matchRanges, st')| none => (#[], currentSt)currentSt := searchSt
match selRange with| none => winBuf := winBuf.push displayLine| some _ =>
let needsStyled := selRange.isSome || !searchMatches.isEmptyif !needsStyled thenwinBuf := winBuf.push displayLineelse
if isSelected && !styleActive thenwinBuf := winBuf.push "\x1b[7m" -- Inverse videostyleActive := trueelse if !isSelected && styleActive then
if isSelected thenif !styleActive thenwinBuf := winBuf.push "\x1b[7m" -- Inverse videostyleActive := trueelse if isMatched thenif !styleActive thenif isCursorMatch thenwinBuf := winBuf.push st.config.searchHighlightCursorStyleelsewinBuf := winBuf.push st.config.searchHighlightStylestyleActive := trueelse if styleActive then
deriving Inhabitedinductive SearchDirection where| forward| backwardderiving Repr, Inhabited, BEqstructure SearchState wherepattern : Stringdirection : SearchDirectionuseBloom : BoollastMatch : Option NatlastSearchOffset : Natcache : Array NatcacheMax : NatlineMatches : Lean.RBMap Row (String × Array (Nat × Nat)) comparelineOrder : Array RowlineCacheMax : NatbloomCache : Lean.RBMap Nat ByteArray comparebloomOrder : Array NatbloomCacheMax : Natderiving Inhabitedinductive RegisterKind where| charwise| linewise| blockwisederiving Repr, Inhabited, BEqstructure Register wherekind : RegisterKindtext : StringblockLines : List StringblockWidth : Nat
import ViE.State.Search
{ s.exitVisualMode with clipboard := some text, message := s!"Yanked selection" }
let reg : Register :=if s.mode == .visualBlock thenlet lines := if text.isEmpty then [] else text.splitOn "\n"let width := lines.foldl (fun m l => max m (ViE.Unicode.stringWidth l)) 0{kind := .blockwisetext := textblockLines := linesblockWidth := width}else{kind := .charwisetext := textblockLines := []blockWidth := 0}{ s.exitVisualMode with clipboard := some reg, message := s!"Yanked selection" }
import ViE.State.Layoutimport ViE.State.Movementimport ViE.Typesimport ViE.Buffer.Contentimport ViE.Data.PieceTableimport ViE.Data.PieceTable.Treenamespace ViEdef searchChunkSize : Nat := 8192def incrementalSearchDebounceMs : Nat := 120def updateSearchCache (state : SearchState) (offset : Nat) : SearchState :=let cache := state.cache.push offsetlet cache :=if cache.size > state.cacheMax thencache.extract (cache.size - state.cacheMax) cache.sizeelsecache{ state with cache := cache }def getCursorOffset (s : EditorState) : Nat :=let buf := s.getActiveBufferlet cursor := s.getCursorViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0def applyMatchOffset (s : EditorState) (offset : Nat) : EditorState :=let buf := s.getActiveBufferlet (r, c) := buf.table.getPointFromOffset offsets.setCursor { row := ⟨r⟩, col := ⟨c⟩ }def startSearch (s : EditorState) (pattern : String) (direction : SearchDirection) (useBloom : Bool) : EditorState :=let cursorOffset := getCursorOffset slet search : SearchState := {pattern := patterndirection := directionuseBloom := useBloomlastMatch := nonelastSearchOffset := cursorOffsetcache := #[]cacheMax := 128lineMatches := Lean.RBMap.emptylineOrder := #[]lineCacheMax := 512bloomCache := Lean.RBMap.emptybloomOrder := #[]bloomCacheMax := s.config.searchBloomCacheMax}{ s with searchState := some search }def startOrUpdateSearch (s : EditorState) (pattern : String) (direction : SearchDirection) (useBloom : Bool) : EditorState :=match s.searchState with| none => startSearch s pattern direction useBloom| some st =>let cursorOffset := getCursorOffset slet st' := {st withpattern := patterndirection := directionuseBloom := useBloomlastMatch := nonelastSearchOffset := cursorOffsetcache := #[]lineMatches := Lean.RBMap.emptylineOrder := #[]}{ s with searchState := some st' }def searchNextOffset (pt : PieceTable) (pattern : ByteArray) (startOffset : Nat) (useBloom : Bool)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=PieceTree.searchNext pt.tree pt pattern startOffset searchChunkSize useBloom cache order cacheMaxdef searchPrevOffset (pt : PieceTable) (pattern : ByteArray) (startExclusive : Nat) (useBloom : Bool)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=PieceTree.searchPrev pt.tree pt pattern startExclusive searchChunkSize useBloom cache order cacheMaxdef findNextMatch (s : EditorState) (directionOverride : Option SearchDirection := none) : EditorState :=match s.searchState with| none => { s with message := "No search pattern" }| some st =>let direction := directionOverride.getD st.directionif st.pattern.isEmpty then{ s with message := "Empty search pattern" }elselet pt := s.getActiveBuffer.tablelet patBytes := st.pattern.toUTF8let startOffset :=match direction with| .forward =>match st.lastMatch with| some m => m + 1| none => getCursorOffset s| .backward =>match st.lastMatch with| some m => m| none => getCursorOffset slet useBloom := st.useBloom && patBytes.size >= 3let (result, bloomCache, bloomOrder) :=match direction with| .forward => searchNextOffset pt patBytes startOffset useBloom st.bloomCache st.bloomOrder st.bloomCacheMax| .backward => searchPrevOffset pt patBytes startOffset useBloom st.bloomCache st.bloomOrder st.bloomCacheMaxlet (result, wrapped, bloomCache, bloomOrder) :=match result, direction with| some r, _ => (some r, false, bloomCache, bloomOrder)| none, .forward =>if startOffset > 0 thenlet (r2, c2, o2) := searchNextOffset pt patBytes 0 useBloom bloomCache bloomOrder st.bloomCacheMax(r2, true, c2, o2)else(none, false, bloomCache, bloomOrder)| none, .backward =>let total := pt.tree.lengthif startOffset < total thenlet (r2, c2, o2) := searchPrevOffset pt patBytes total useBloom bloomCache bloomOrder st.bloomCacheMax(r2, true, c2, o2)else(none, false, bloomCache, bloomOrder)match result with| none =>let st' := { st with bloomCache := bloomCache, bloomOrder := bloomOrder }{ s with searchState := some st', message := s!"Pattern not found: {st.pattern}" }| some off =>let s' := applyMatchOffset s offlet st' := updateSearchCache { st with lastMatch := some off, bloomCache := bloomCache, bloomOrder := bloomOrder } offlet st'' := { st' with direction := direction }let bloomTag := if useBloom then " [bloom]" else ""let msg :=if wrapped thens!"Wrapped: {st.pattern}{bloomTag}"elses!"Match: {st.pattern}{bloomTag}"{ s' with searchState := some st'', message := msg }def runIncrementalSearch (s : EditorState) : EditorState :=if s.mode != .searchForward && s.mode != .searchBackward thenselselet pattern := s.inputState.commandBufferif pattern.isEmpty thenselselet direction := if s.mode == .searchBackward then SearchDirection.backward else SearchDirection.forwardlet s' := startOrUpdateSearch s pattern direction falsefindNextMatch s' (some direction)def maybeRunIncrementalSearch (s : EditorState) (now : Nat) : EditorState :=if s.inputState.pendingSearch && now - s.inputState.lastSearchInputTime >= incrementalSearchDebounceMs thenlet s' := runIncrementalSearch s{ s' withdirty := trueinputState := { s'.inputState with pendingSearch := false, lastSearchRunTime := now }}elsesend ViE
let deletedText :=match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with| some startOff, some endOff =>if cursor.col.val < lineLen && endOff > startOff thenPieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.tableelse""| _, _ => ""
let newBuffer := s'.getActiveBuffer
let s'' :=if deletedText.isEmpty thens'elselet reg : Register := {kind := .charwisetext := deletedTextblockLines := []blockWidth := 0}{ s' with clipboard := some reg }let newBuffer := s''.getActiveBuffer
let buffer := s.getActiveBufferlet (startOffOpt, endOffOpt) :=match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with| some off1, some off2 => (some (min off1 off2), some (max off1 off2))| _, _ => (none, none)let deletedText :=match (startOffOpt, endOffOpt) with| (some startOff, some endOff) =>if endOff > startOff thenPieceTree.getSubstring buffer.table.tree startOff (endOff - startOff) buffer.tableelse""| _ => ""
match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with| some off1, some off2 =>let startOff := min off1 off2let endOff := max off1 off2
match (startOffOpt, endOffOpt) with| (some startOff, some endOff) =>
{ s'' with inputState := { s''.inputState with previousKey := none } }
let s''' :=if deletedText.isEmpty thens''elselet reg : Register := {kind := .charwisetext := deletedTextblockLines := []blockWidth := 0}{ s'' with clipboard := some reg }{ s''' with inputState := { s'''.inputState with previousKey := none } }
{ s with clipboard := (some content : Option String), message := "Yanked 1 line" }
let reg : Register := {kind := .linewisetext := contentblockLines := []blockWidth := 0}{ s with clipboard := some reg, message := "Yanked 1 line" }def EditorState.ensureLineCount (s : EditorState) (count : Nat) : EditorState :=s.updateActiveBuffer fun buffer =>let lineCount := buffer.table.lineCountif count <= lineCount thenbufferelselet missing := count - lineCountlet newlines := String.ofList (List.replicate missing '\n')let len := buffer.table.tree.length{ buffer with table := buffer.table.insert len newlines len, dirty := true }def EditorState.pasteCharwise (s : EditorState) (text : String) (after : Bool) : EditorState :=let cursor := s.getCursorlet line := ViE.getLineFromBuffer s.getActiveBuffer cursor.row |>.getD ""let lineWidth := ViE.Unicode.stringWidth linelet targetCol :=if after thenif cursor.col.val < lineWidth thenViE.Unicode.nextDisplayCol line cursor.col.valelsecursor.col.valelsecursor.col.vallet s' := s.updateActiveBuffer fun buffer =>match ViE.getOffsetFromPointInBuffer buffer cursor.row.val targetCol with| some offset => { buffer with table := buffer.table.insert offset text offset, dirty := true }| none => bufferlet lines := text.splitOn "\n"let lastLine := lines.getLastD ""let lastWidth := ViE.Unicode.stringWidth lastLinelet rowDelta := if lines.length > 0 then lines.length - 1 else 0let newRow := cursor.row.val + rowDeltalet newCol :=if lines.length <= 1 thenif lastWidth == 0 then targetCol else targetCol + lastWidth - 1elseif lastWidth == 0 then 0 else lastWidth - 1s'.setCursor { row := ⟨newRow⟩, col := ⟨newCol⟩ }def firstNonBlankCol (line : String) : Nat :=let rec loop (cs : List Char) (col : Nat) : Nat :=match cs with| [] => 0| c :: rest =>if c == ' ' || c == '\t' thenloop rest (col + ViE.Unicode.charWidth c)elsecolloop line.toList 0def EditorState.pasteLinewise (s : EditorState) (text : String) (below : Bool) : EditorState :=let cursor := s.getCursorlet row := if below then cursor.row.val + 1 else cursor.row.vallet s' := s.updateActiveBuffer fun buffer =>-- Determine insert offset.-- Try start of target line. If EOF, append.let (offset, textToInsert) := match ViE.getOffsetFromPointInBuffer buffer row 0 with| some off => (off, text)| none =>let len := buffer.table.tree.lengthif len > 0 thenif !PieceTable.endsWithNewline buffer.table then(len, "\n" ++ text)else(len, text)else (0, text)let pt := buffer.table.commit{ buffer with table := pt.insert offset textToInsert offset, dirty := true }let newRow := if below then cursor.row.val + 1 else cursor.row.vallet lineStr := ViE.getLineFromBuffer s'.getActiveBuffer ⟨newRow⟩ |>.getD ""let col := firstNonBlankCol lineStrs'.setCursor { row := ⟨newRow⟩, col := ⟨col⟩ }def EditorState.pasteBlockwise (s : EditorState) (reg : Register) (after : Bool) : EditorState :=let cursor := s.getCursorlet line := ViE.getLineFromBuffer s.getActiveBuffer cursor.row |>.getD ""let lineWidth := ViE.Unicode.stringWidth linelet baseCol :=if after thenif cursor.col.val < lineWidth thenViE.Unicode.nextDisplayCol line cursor.col.valelsecursor.col.valelsecursor.col.vallet lines :=if reg.blockLines.isEmpty thenif reg.text.isEmpty then [] else reg.text.splitOn "\n"elsereg.blockLineslet targetLineCount := cursor.row.val + lines.lengthlet s1 := s.ensureLineCount targetLineCountlet s2 := s1.updateActiveBuffer fun buffer =>let rec apply (buf : FileBuffer) (idx : Nat) (ls : List String) : FileBuffer :=match ls with| [] => buf| l :: rest =>let row := cursor.row.val + idxlet lineStr := ViE.getLineFromBuffer buf ⟨row⟩ |>.getD ""let lineW := ViE.Unicode.stringWidth lineStrlet targetCol := baseCollet (buf1, offset) :=if targetCol > lineW thenlet pad := targetCol - lineWlet padStr := String.ofList (List.replicate pad ' ')let insertOff := ViE.getOffsetFromPointInBuffer buf row lineW |>.getD (buf.table.tree.length)let buf' := { buf with table := buf.table.insert insertOff padStr insertOff, dirty := true }let off' := ViE.getOffsetFromPointInBuffer buf' row targetCol |>.getD insertOff(buf', off')elselet off := ViE.getOffsetFromPointInBuffer buf row targetCol |>.getD 0(buf, off)let buf2 := { buf1 with table := buf1.table.insert offset l offset, dirty := true }apply buf2 (idx + 1) restapply buffer 0 liness2.setCursor { row := cursor.row, col := ⟨baseCol⟩ }
| some text =>let cursor := s.getCursorlet s' := s.updateActiveBuffer fun buffer =>-- Determine insert offset.-- Try start of next line. If EOF, append.let (offset, textToInsert) := match ViE.getOffsetFromPointInBuffer buffer (cursor.row.val + 1) 0 with| some off => (off, text)| none =>let len := buffer.table.tree.lengthif len > 0 then-- Check if buffer ends with newline to avoid merging-- (Optimization: ideally check last char directly)if !PieceTable.endsWithNewline buffer.table then(len, "\n" ++ text)else(len, text)else (0, text)
| some reg =>match reg.kind with| .linewise => s.pasteLinewise reg.text true| .charwise => s.pasteCharwise reg.text true| .blockwise => s.pasteBlockwise reg true
-- For paste, undo should restore cursor to insertion pointlet pt := buffer.table.commit{ buffer with table := pt.insert offset textToInsert offsetdirty := true }s'.setCursor { row := ⟨cursor.row.val + 1⟩, col := 0 }
| some text =>let cursor := s.getCursorlet s' := s.updateActiveBuffer fun buffer =>let offset := match ViE.getOffsetFromPointInBuffer buffer cursor.row.val 0 with| some off => off| none => 0let pt := buffer.table.commitlet textStr : String := text{ buffer with table := pt.insert offset textStr offsetdirty := true }s'.setCursor { cursor with col := 0 }
| some reg =>match reg.kind with| .linewise => s.pasteLinewise reg.text false| .charwise => s.pasteCharwise reg.text false| .blockwise => s.pasteBlockwise reg false
| Key.char '/' =>pure {s withmode := Mode.searchForwardinputState := {s.inputState withcommandBuffer := ""countBuffer := ""previousKey := nonependingSearch := false}}| Key.char '?' =>pure {s withmode := Mode.searchBackwardinputState := {s.inputState withcommandBuffer := ""countBuffer := ""previousKey := nonependingSearch := false}}
| Key.char 'n' => pure $ clearInput (ViE.findNextMatch s)| Key.char 'N' =>let overrideDir :=match s.searchState with| some st =>if st.direction == .forward then some SearchDirection.backward else some SearchDirection.forward| none => nonepure $ clearInput (ViE.findNextMatch s overrideDir)
| _ => return statedef handleSearchInput (state : EditorState) (k : Key) : IO EditorState := domatch k with| Key.esc =>return {state withmode := .normalinputState := { state.inputState with commandBuffer := "", pendingSearch := false }}| Key.enter =>let pattern := state.inputState.commandBufferif pattern.isEmpty thenreturn {state withmode := .normalmessage := "Empty search pattern"inputState := { state.inputState with commandBuffer := "", pendingSearch := false }}elselet direction := if state.mode == .searchBackward then SearchDirection.backward else SearchDirection.forwardlet s' :=match state.searchState with| some st =>if st.pattern == pattern && st.direction == direction thenstateelseViE.startOrUpdateSearch state pattern direction false| none =>ViE.startOrUpdateSearch state pattern direction falselet s'' := ViE.findNextMatch s' (some direction)return {s'' withmode := .normalinputState := { s''.inputState with commandBuffer := "", pendingSearch := false }}| Key.backspace =>if state.inputState.commandBuffer.length > 0 thenlet newCmd := state.inputState.commandBuffer.dropEnd 1let now ← IO.monoMsNowlet s1 := {state withinputState := {state.inputState withcommandBuffer := newCmd.toStringlastSearchInputTime := nowpendingSearch := true}}if now - state.inputState.lastSearchRunTime >= ViE.incrementalSearchDebounceMs thenlet s2 := ViE.runIncrementalSearch s1return { s2 with inputState := { s2.inputState with pendingSearch := false, lastSearchRunTime := now } }elsereturn s1elsereturn state| Key.char c =>let now ← IO.monoMsNowlet s1 := {state withinputState := {state.inputState withcommandBuffer := state.inputState.commandBuffer.push clastSearchInputTime := nowpendingSearch := true}}if now - state.inputState.lastSearchRunTime >= ViE.incrementalSearchDebounceMs thenlet s2 := ViE.runIncrementalSearch s1return { s2 with inputState := { s2.inputState with pendingSearch := false, lastSearchRunTime := now } }elsereturn s1
let tree := PieceTree.fromPieces pieces
let tmpPt : PieceTable := { original := bytes, addBuffers := #[], tree := PieceTree.empty, undoStack := [], redoStack := [], undoStackCount := 0, redoStackCount := 0, undoLimit := 100, lastInsert := none }let tree := PieceTree.fromPieces pieces tmpPt
let mid := PieceTree.fromPieces newPieceslet newTree := PieceTree.concat (PieceTree.concat l mid) r
let mid := PieceTree.fromPieces newPieces pt'let newTree := PieceTree.concat (PieceTree.concat l mid pt') r pt'
}/-- Insert text without touching undo/redo stacks (internal for bulk edits). -/def PieceTable.insertRaw (pt : PieceTable) (offset : Nat) (text : String) : PieceTable :=if text.isEmpty then ptelselet (pt', newPieces) := PieceTableHelper.appendText pt textlet (l, r) := PieceTree.split pt.tree offset pt'let mid := PieceTree.fromPieces newPieces pt'let newTree := PieceTree.concat (PieceTree.concat l mid pt') r pt'{ pt' with tree := newTree, lastInsert := none }/-- Delete a range without touching undo/redo stacks (internal for bulk edits). -/def PieceTable.deleteRaw (pt : PieceTable) (offset : Nat) (length : Nat) : PieceTable :=if length == 0 then ptelselet newTree := PieceTree.delete pt.tree offset length pt{ pt with tree := newTree, lastInsert := none }/-- Apply a list of replacements as a single undoable edit. -/def PieceTable.applyReplacements (pt : PieceTable) (cursorOffset : Nat) (replacements : Array (Nat × Nat)) (newText : String) : PieceTable :=if replacements.isEmpty thenptelselet oldTree := pt.treelet pt' := Id.run dolet mut acc := ptfor (startOff, endOff) in replacements.reverse dolet len := endOff - startOffacc := acc.deleteRaw startOff lenacc := acc.insertRaw startOff newTextreturn acclet stack := (oldTree, cursorOffset) :: pt'.undoStacklet newCount := pt'.undoStackCount + 1let (finalStack, finalCount) :=if newCount > pt'.undoLimit then(stack.take pt'.undoLimit, pt'.undoLimit)else(stack, newCount){ pt' withundoStack := finalStackundoStackCount := finalCountredoStack := []redoStackCount := 0lastInsert := none
def searchMetaOf (t : ViE.PieceTree) : ViE.SearchBloom :=match t with| ViE.PieceTree.empty => ViE.SearchBloom.empty| ViE.PieceTree.leaf _ _ m => m| ViE.PieceTree.internal _ _ m => mdef bloomOr (a b : ByteArray) : ByteArray := Id.run dolet mut out := alet size := min a.size b.sizefor i in [0:size] doout := out.set! i (out[i]! ||| b[i]!)outdef bloomSetBit (bloom : ByteArray) (idx : Nat) : ByteArray :=let byteIdx := idx / 8let bitIdx := idx % 8if byteIdx < bloom.size thenlet cur := bloom[byteIdx]!let mask : UInt8 := UInt8.ofNat (1 <<< bitIdx)bloom.set! byteIdx (cur ||| mask)elsebloomdef bloomGetBit (bloom : ByteArray) (idx : Nat) : Bool :=let byteIdx := idx / 8let bitIdx := idx % 8if byteIdx < bloom.size thenlet cur := bloom[byteIdx]!let mask : UInt8 := UInt8.ofNat (1 <<< bitIdx)(cur &&& mask) != 0elsefalsedef hash1 (b0 b1 b2 : UInt8) : Nat :=(b0.toNat * 961 + b1.toNat * 31 + b2.toNat) % ViE.BloomBitsdef hash2 (b0 b1 b2 : UInt8) : Nat :=(b0.toNat * 17161 + b1.toNat * 131 + b2.toNat) % ViE.BloomBitsdef addTrigramToBloom (bloom : ByteArray) (b0 b1 b2 : UInt8) : ByteArray :=let h1 := hash1 b0 b1 b2let h2 := hash2 b0 b1 b2bloomSetBit (bloomSetBit bloom h1) h2def addTrigramsFromArray (bloom : ByteArray) (arr : Array UInt8) : ByteArray := Id.run doif arr.size < 3 thenreturn bloomlet limit := arr.size - 2let mut out := bloomfor i in [0:limit] doout := addTrigramToBloom out arr[i]! arr[i + 1]! arr[i + 2]!return outdef takeFirstBytes (arr : Array UInt8) (n : Nat) : Array UInt8 :=if arr.size <= n then arr else arr.extract 0 ndef takeLastBytes (arr : Array UInt8) (n : Nat) : Array UInt8 :=if arr.size <= n then arr else arr.extract (arr.size - n) arr.sizepartial def buildPrefixBytes (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : Array UInt8 :=let rec loop (i : Nat) (acc : Array UInt8) : Array UInt8 :=if i >= pieces.size || acc.size >= 2 thenaccelselet p := pieces[i]!let buf := PieceTableHelper.getBuffer pt p.sourcelet slice := buf.extract p.start (p.start + p.length)if slice.size > 0 thenlet need := 2 - acc.sizelet take := takeFirstBytes slice.data needloop (i + 1) (acc ++ take)elseloop (i + 1) accloop 0 #[]partial def buildSuffixBytes (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : Array UInt8 :=let rec loop (i : Nat) (acc : Array UInt8) : Array UInt8 :=if i == 0 || acc.size >= 2 thenaccelselet idx := i - 1let p := pieces[idx]!let buf := PieceTableHelper.getBuffer pt p.sourcelet slice := buf.extract p.start (p.start + p.length)if slice.size > 0 thenlet need := 2 - acc.sizelet take := takeLastBytes slice.data needloop idx (take ++ acc)elseloop idx accloop pieces.size #[]def addBytesToBloom (bloom : ByteArray) (carry : Array UInt8) (bytes : ByteArray) : (ByteArray × Array UInt8) :=let arr := carry ++ bytes.datalet bloom' := addTrigramsFromArray bloom arrlet carry' := takeLastBytes arr 2(bloom', carry')def addBoundaryTrigrams (bloom : ByteArray) (leftSuffix rightPrefix : Array UInt8) : ByteArray :=let combined := leftSuffix ++ rightPrefixaddTrigramsFromArray bloom combineddef buildBloomForPieces (pieces : Array ViE.Piece) (pt : ViE.PieceTable) : ViE.SearchBloom := Id.run doif !ViE.BloomBuildLeafBits thenlet prefixBytes := buildPrefixBytes pieces ptlet suffixBytes := buildSuffixBytes pieces ptreturn { bits := ViE.SearchBloom.empty.bits, prefixBytes := prefixBytes, suffixBytes := suffixBytes }elselet mut bits := ViE.SearchBloom.empty.bitslet mut carry : Array UInt8 := #[]let mut prefixBytes : Array UInt8 := #[]for p in pieces dolet buf := PieceTableHelper.getBuffer pt p.sourcelet slice := buf.extract p.start (p.start + p.length)if prefixBytes.size < 2 && slice.size > 0 thenlet need := 2 - prefixBytes.sizelet arr := slice.datalet take := takeFirstBytes arr needprefixBytes := prefixBytes ++ takelet (bits', carry') := addBytesToBloom bits carry slicebits := bits'carry := carry'return { bits := bits, prefixBytes := prefixBytes, suffixBytes := carry }
def bloomIsEmpty (bloom : ByteArray) : Bool :=bloom.data.all (fun b => b == 0)def combineBloom (left right : ViE.SearchBloom) : ViE.SearchBloom :=let pref :=if left.prefixBytes.size >= 2 then left.prefixByteselse takeFirstBytes (left.prefixBytes ++ right.prefixBytes) 2let suf :=if right.suffixBytes.size >= 2 then right.suffixByteselse takeLastBytes (left.suffixBytes ++ right.suffixBytes) 2-- If any child bloom is empty (unknown), keep bits empty to avoid false negatives.if bloomIsEmpty left.bits || bloomIsEmpty right.bits then{ bits := ViE.SearchBloom.empty.bits, prefixBytes := pref, suffixBytes := suf }elselet bits := bloomOr left.bits right.bitslet bits := addBoundaryTrigrams bits left.suffixBytes right.prefixBytes{ bits := bits, prefixBytes := pref, suffixBytes := suf }def buildBloomForChildren (children : Array ViE.PieceTree) : ViE.SearchBloom := Id.run doif children.isEmpty thenreturn ViE.SearchBloom.emptylet mut acc := searchMetaOf children[0]!for i in [1:children.size] doacc := combineBloom acc (searchMetaOf children[i]!)return accdef patternTrigramHashes (pattern : ByteArray) : Array (Nat × Nat) := Id.run doif pattern.size < 3 thenreturn #[]let arr := pattern.datalet limit := pattern.size - 2let mut hashes : Array (Nat × Nat) := #[]for i in [0:limit] dolet b0 := arr[i]!let b1 := arr[i + 1]!let b2 := arr[i + 2]!hashes := hashes.push (hash1 b0 b1 b2, hash2 b0 b1 b2)return hashesdef bloomMayContain (bloom : ByteArray) (hashes : Array (Nat × Nat)) : Bool :=if hashes.isEmpty thentrueelse if bloomIsEmpty bloom then-- Empty bloom means "unknown", do not prune.trueelsehashes.all (fun (h1, h2) => bloomGetBit bloom h1 && bloomGetBit bloom h2)def cacheInsert (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (maxSize : Nat) (key : Nat) (value : ByteArray): (Lean.RBMap Nat ByteArray compare × Array Nat) :=let cache := cache.insert key valuelet order := if order.contains key then order else order.push keyif order.size > maxSize thenlet dropCount := order.size - maxSizelet evicted := order.extract 0 dropCountlet order := order.extract dropCount order.sizelet cache := evicted.foldl (fun acc k => acc.erase k) cache(cache, order)else(cache, order)def leafBloomBitsWithCache (pieces : Array ViE.Piece) (pt : ViE.PieceTable) (leafOffset : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (maxSize : Nat): (ByteArray × Lean.RBMap Nat ByteArray compare × Array Nat) :=match cache.find? leafOffset with| some bits => (bits, cache, order)| none =>let bits := (buildBloomForPieces pieces pt).bitslet (cache', order') := cacheInsert cache order maxSize leafOffset bits(bits, cache', order')
| ViE.PieceTree.leaf .. , ViE.PieceTree.internal .. => concat (mkInternal #[l]) r| ViE.PieceTree.internal .. , ViE.PieceTree.leaf .. => concat l (mkInternal #[r])
| ViE.PieceTree.leaf .. , ViE.PieceTree.internal .. => concat (mkInternal #[l]) r pt| ViE.PieceTree.internal .. , ViE.PieceTree.leaf .. => concat l (mkInternal #[r]) pt
/-- Get substring from tree -/partial def getSubstring (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : String :=
/-- Get bytes from tree -/partial def getBytes (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : ByteArray :=
let combined := chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])String.fromUTF8! combined
chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])/-- Get substring from tree -/partial def getSubstring (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : String :=String.fromUTF8! (getBytes t offset len pt)
partial def maximalSuffixLoop (x : ByteArray) (useLe : Bool) (m ms j k p : Int) : (Int × Int) :=if j + k >= m then(ms, p)elselet a := x[Int.toNat (j + k)]!let b := x[Int.toNat (ms + k)]!if useLe thenif a < b thenmaximalSuffixLoop x useLe m ms (j + k) 1 (j + k - ms)else if a == b thenif k != p thenmaximalSuffixLoop x useLe m ms j (k + 1) pelsemaximalSuffixLoop x useLe m ms (j + p) 1 pelsemaximalSuffixLoop x useLe m j (j + 1) 1 1elseif a > b thenmaximalSuffixLoop x useLe m ms (j + k) 1 (j + k - ms)else if a == b thenif k != p thenmaximalSuffixLoop x useLe m ms j (k + 1) pelsemaximalSuffixLoop x useLe m ms (j + p) 1 pelsemaximalSuffixLoop x useLe m j (j + 1) 1 1def maximalSuffix (x : ByteArray) (useLe : Bool) : (Int × Int) :=let m : Int := x.sizemaximalSuffixLoop x useLe m (-1) 0 1 1partial def twoWayForward1 (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) : Int :=if j >= n thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayForward1 haystack needle i n (j + 1)elsejpartial def twoWayBackward1 (haystack needle : ByteArray) (i : Nat) (mem : Int) (j : Int) : Int :=if j <= mem thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayBackward1 haystack needle i mem (j - 1)elsejpartial def twoWayForward2 (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) : Int :=if j >= n thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayForward2 haystack needle i n (j + 1)elsejpartial def twoWayBackward2 (haystack needle : ByteArray) (i : Nat) (j : Int) : Int :=if j < 0 thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayBackward2 haystack needle i (j - 1)elsejpartial def twoWayShortLoop (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) (mem : Int) : Option Nat :=if i > maxStart thennoneelselet j0 := max (Int.ofNat msNat) mem + 1let j := twoWayForward1 haystack needle i n j0if j >= n thenlet j2 := twoWayBackward1 haystack needle i mem (Int.ofNat msNat)if j2 <= mem thensome ielselet nextI := i + pNatlet nextMem := Int.ofNat (n - pNat - 1)twoWayShortLoop haystack needle start maxStart msNat pNat n nextI nextMemelselet shift := Int.toNat (j - Int.ofNat msNat)twoWayShortLoop haystack needle start maxStart msNat pNat n (i + shift) (-1)partial def twoWayLongLoop (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) : Option Nat :=if i > maxStart thennoneelselet j := twoWayForward2 haystack needle i n (Int.ofNat (msNat + 1))if j >= n thenlet j2 := twoWayBackward2 haystack needle i (Int.ofNat msNat)if j2 < 0 thensome ielselet nextI := i + pNattwoWayLongLoop haystack needle start maxStart msNat pNat n nextIelselet shift := Int.toNat (j - Int.ofNat msNat)twoWayLongLoop haystack needle start maxStart msNat pNat n (i + shift)def twoWaySearch (haystack : ByteArray) (needle : ByteArray) (start : Nat) : Option Nat :=let n := needle.sizelet h := haystack.sizeif n == 0 thensome startelse if h < n || start + n > h thennoneelselet (ms1, p1) := maximalSuffix needle truelet (ms2, p2) := maximalSuffix needle falselet (ms, p) := if ms1 > ms2 then (ms1, p1) else (ms2, p2)let msNat := Int.toNat mslet pNat := Int.toNat plet maxStart := h - nlet rec prefixEqual (i : Nat) : Bool :=if ms < 0 then trueelse if i > msNat then trueelse if i + pNat >= n then falseelse if needle[i]! == needle[i + pNat]! thenprefixEqual (i + 1)elsefalselet shortPeriod := prefixEqual 0if shortPeriod thentwoWayShortLoop haystack needle start maxStart msNat pNat n start (-1)elsetwoWayLongLoop haystack needle start maxStart msNat pNat n startpartial def findPatternInBytes (haystack : ByteArray) (needle : ByteArray) (start : Nat) : Option Nat :=twoWaySearch haystack needle startpartial def findLastPatternInBytes (haystack : ByteArray) (needle : ByteArray) : Option Nat :=let n := needle.sizelet h := haystack.sizeif n == 0 thensome 0else if h < n thennoneelselet maxStart := h - nlet rec loop (i : Nat) (last : Option Nat) : Option Nat :=if i > maxStart then lastelsematch findPatternInBytes haystack needle i with| some idx =>if idx > maxStart then lastelse loop (idx + 1) (some idx)| none => lastloop 0 none/-- Search forward for a byte pattern from a given offset -/partial def searchNext (t : ViE.PieceTree) (pt : ViE.PieceTable) (pattern : ByteArray) (startOffset : Nat) (chunkSize : Nat)(useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=if pattern.size == 0 then(none, cache, order)elselet total := length tif startOffset >= total then(none, cache, order)elseif pattern.size < 3 || !useBloom thenlet chunkLen := max chunkSize pattern.sizelet overlap := pattern.size - 1let rec loop (offset : Nat) : Option Nat :=if offset >= total then noneelselet remaining := total - offsetlet readLen := min chunkLen remainingif readLen < pattern.size thennoneelselet bytes := getBytes t offset readLen ptmatch findPatternInBytes bytes pattern 0 with| some idx => some (offset + idx)| none =>if offset + readLen >= total then noneelselet nextOffset := offset + (readLen - overlap)loop nextOffset(loop startOffset, cache, order)elselet hashes := patternTrigramHashes patternlet rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=if baseOffset + length node <= startOffset then(none, cache, order)elsematch node with| ViE.PieceTree.empty => (none, cache, order)| ViE.PieceTree.leaf _ _ _ =>let relStart := if startOffset > baseOffset then startOffset - baseOffset else 0let remain := length node - relStartif remain < pattern.size then(none, cache, order)elsematch node with| ViE.PieceTree.leaf pieces _ m =>let (bits, cache, order) :=if bloomIsEmpty m.bits thenleafBloomBitsWithCache pieces pt baseOffset cache order cacheMaxelse(m.bits, cache, order)if !bloomMayContain bits hashes then(none, cache, order)elselet bytes := getBytes node relStart remain ptmatch findPatternInBytes bytes pattern 0 with| some idx => (some (baseOffset + relStart + idx), cache, order)| none => (none, cache, order)| _ => (none, cache, order)| ViE.PieceTree.internal children _ _ =>let rec loop (i : Nat) (offset : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=if i >= children.size then(none, cache, order)elselet child := children[i]!let childLen := length childlet childEnd := offset + childLenif childEnd <= startOffset thenloop (i + 1) childEnd cache orderelsematch searchNode child offset cache order with| (some res, cache, order) => (some res, cache, order)| (none, cache, order) => loop (i + 1) childEnd cache orderloop 0 baseOffset cache ordersearchNode t 0 cache order/-- Search backward for a byte pattern ending before startExclusive -/partial def searchPrev (t : ViE.PieceTree) (pt : ViE.PieceTable) (pattern : ByteArray) (startExclusive : Nat) (chunkSize : Nat)(useBloom : Bool) (cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (cacheMax : Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=if pattern.size == 0 then(none, cache, order)elselet total := length tlet end0 := min startExclusive totalif end0 == 0 then(none, cache, order)else if pattern.size < 3 || !useBloom thenlet chunkLen := max chunkSize pattern.sizelet overlap := pattern.size - 1let rec loop (endOffset : Nat) : Option Nat :=if endOffset == 0 then noneelselet start := if endOffset > chunkLen then endOffset - chunkLen else 0let readLen := endOffset - startif readLen < pattern.size thenif start == 0 then none else loop (start + overlap)elselet bytes := getBytes t start readLen ptmatch findLastPatternInBytes bytes pattern with| some idx =>let pos := start + idxif pos < endOffset then some pos else none| none =>if start == 0 then none else loop (start + overlap)(loop end0, cache, order)elselet hashes := patternTrigramHashes patternlet rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=if baseOffset >= end0 then(none, cache, order)elsematch node with| ViE.PieceTree.empty => (none, cache, order)| ViE.PieceTree.leaf _ _ _ =>let relEnd := min (end0 - baseOffset) (length node)if relEnd < pattern.size then(none, cache, order)elsematch node with| ViE.PieceTree.leaf pieces _ m =>let (bits, cache, order) :=if bloomIsEmpty m.bits thenleafBloomBitsWithCache pieces pt baseOffset cache order cacheMaxelse(m.bits, cache, order)if !bloomMayContain bits hashes then(none, cache, order)elselet bytes := getBytes node 0 relEnd ptmatch findLastPatternInBytes bytes pattern with| some idx => (some (baseOffset + idx), cache, order)| none => (none, cache, order)| _ => (none, cache, order)| ViE.PieceTree.internal children _ _ =>let spans : Array (ViE.PieceTree × Nat) := Id.run dolet mut acc : Array (ViE.PieceTree × Nat) := #[]let mut offset := baseOffsetfor child in children doacc := acc.push (child, offset)offset := offset + length childreturn acclet rec loop (i : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=if i >= spans.size then(none, cache, order)elselet j := spans.size - 1 - ilet (child, childOffset) := spans[j]!if childOffset >= end0 thenloop (i + 1) cache orderelsematch searchNode child childOffset cache order with| (some res, cache, order) =>if res < end0 then (some res, cache, order) else loop (i + 1) cache order| (none, cache, order) => loop (i + 1) cache orderloop 0 cache ordersearchNode t 0 cache order
/-- Bloom filter bit size for trigram indexing. -/def BloomBits : Nat := 4096/-- Bloom filter byte size. -/def BloomBytes : Nat := BloomBits / 8/-- Build full bloom bits for leaf nodes (startup cost). -/def BloomBuildLeafBits : Bool := false/-- Search metadata for a piece tree node. -/structure SearchBloom wherebits : ByteArrayprefixBytes : Array UInt8suffixBytes : Array UInt8deriving Inhabiteddef SearchBloom.empty : SearchBloom := {bits := ByteArray.mk (Array.replicate BloomBytes (0 : UInt8)),prefixBytes := #[],suffixBytes := #[]}
| leaf (pieces : Array Piece) (stats : Stats)| internal (children : Array PieceTree) (stats : Stats)
| leaf (pieces : Array Piece) (stats : Stats) (searchMeta : SearchBloom)| internal (children : Array PieceTree) (stats : Stats) (searchMeta : SearchBloom)
def cmdBloom (args : List String) (state : EditorState) : IO EditorState := dolet (direction, pattern) :=match args with| [] => (SearchDirection.forward, "")| [p] =>if p.startsWith "/" then(SearchDirection.forward, (p.drop 1).toString)else if p.startsWith "?" then(SearchDirection.backward, (p.drop 1).toString)else(SearchDirection.forward, p)| p :: rest =>let full := String.intercalate " " (p :: rest)if full.startsWith "/" then(SearchDirection.forward, (full.drop 1).toString)else if full.startsWith "?" then(SearchDirection.backward, (full.drop 1).toString)else(SearchDirection.forward, full)if pattern.isEmpty thenreturn { state with message := "Empty search pattern" }elselet s' := ViE.startOrUpdateSearch state pattern direction truelet s'' := ViE.findNextMatch s' (some direction)return s''
partial def collectMatchesInBytes (haystack : ByteArray) (needle : ByteArray) : Array (Nat × Nat) :=let n := needle.sizelet h := haystack.sizeif n == 0 || h < n then#[]elselet rec loop (i : Nat) (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=if i + n > h thenaccelsematch ViE.PieceTree.findPatternInBytes haystack needle i with| some idx =>if idx + n > h thenaccelseloop (idx + n) (acc.push (idx, idx + n))| none => accloop 0 #[]partial def collectMatchesInPieceTable (pt : PieceTable) (pattern : ByteArray) : Array (Nat × Nat) :=let n := pattern.sizeif n == 0 then#[]elselet total := pt.tree.lengthlet rec loop (offset : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat)(acc : Array (Nat × Nat)) : Array (Nat × Nat) :=if offset >= total thenaccelselet (res, cache', order') :=ViE.PieceTree.searchNext pt.tree pt pattern offset ViE.searchChunkSize false cache order 0match res with| some idx =>if idx + n > total thenaccelseloop (idx + n) cache' order' (acc.push (idx, idx + n))| none => accloop 0 Lean.RBMap.empty #[] #[]def replaceFirstInLine (line : String) (old : String) (new : String) : String :=if old.isEmpty thenlineelselet parts := line.splitOn oldmatch parts with| [] => line| p :: rest =>if rest.isEmpty thenlineelsep ++ new ++ (String.intercalate old rest)def replaceAllInLine (line : String) (old : String) (new : String) : String :=if old.isEmpty thenlineelseString.intercalate new (line.splitOn old)def parseSubstitute (cmd : String) : Option (Bool × String × String × String) :=let (isGlobal, rest) :=if cmd.startsWith "%s/" then(true, (cmd.drop 3).toString)else if cmd.startsWith "s/" then(false, (cmd.drop 2).toString)else(false, "")if rest.isEmpty thennoneelselet parts := rest.splitOn "/"match parts with| old :: new :: flagsParts =>let flags := String.intercalate "/" flagsPartssome (isGlobal, old, new, flags)| _ => nonedef parseGlobal (cmd : String) : Option (Bool × String × String) :=if cmd.startsWith "g/" || cmd.startsWith "v/" thenlet isInvert := cmd.startsWith "v/"let rest := (cmd.drop 2).toStringlet parts := rest.splitOn "/"match parts with| pat :: cmdParts =>let subcmd := String.intercalate "/" cmdPartssome (isInvert, pat, (subcmd.trimAscii).toString)| _ => noneelsenonedef lineRangeWithNewline (pt : PieceTable) (row : Nat) : Option (Nat × Nat) :=match pt.getLineRange row with| some (startOff, len) =>let endOff := startOff + lenif endOff < pt.tree.length thenlet b := ViE.PieceTree.getBytes pt.tree endOff 1 ptif b.size == 1 && b[0]! == (UInt8.ofNat 10) thensome (startOff, len + 1)elsesome (startOff, len)elsesome (startOff, len)| none => none
def collectMatchesInLine (pt : PieceTable) (row : Nat) (pattern : ByteArray) : Array (Nat × Nat) :=match pt.getLineRange row with| some (startOff, len) =>let bytes := ViE.PieceTree.getBytes pt.tree startOff len ptlet localMatches := collectMatchesInBytes bytes patternlocalMatches.map (fun (s, e) => (startOff + s, startOff + e))| none => #[]def execGlobal (cmd : String) (state : EditorState) : EditorState :=match parseGlobal cmd with| none => { state with message := s!"Invalid global: {cmd}" }| some (isInvert, pat, subcmd) =>if pat.isEmpty then{ state with message := "Empty global pattern" }elselet buf := state.getActiveBufferlet cursor := state.getCursorlet cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0let patBytes := pat.toUTF8let lineCount := buf.lineCountlet matchingRows : Array Nat := Id.run dolet mut rows : Array Nat := #[]for row in [0:lineCount] dolet hasMatch := (collectMatchesInLine buf.table row patBytes).size > 0if (if isInvert then !hasMatch else hasMatch) thenrows := rows.push rowreturn rowsif subcmd == "d" thenlet ranges : Array (Nat × Nat) := Id.run dolet mut acc : Array (Nat × Nat) := #[]for row in matchingRows domatch lineRangeWithNewline buf.table row with| some (startOff, len) => acc := acc.push (startOff, startOff + len)| none => pure ()return acclet newTable := buf.table.applyDeletions cursorOffset rangeslet newBuf := { buf with table := newTable, dirty := true }state.updateActiveBuffer (fun _ => newBuf)else if subcmd.startsWith "s/" thenmatch parseSubstitute subcmd with| none => { state with message := s!"Invalid substitute: {subcmd}" }| some (_isGlobal, old, new, flags) =>if old.isEmpty then{ state with message := "Empty substitute pattern" }elselet doGlobal := flags.contains 'g'let oldBytes := old.toUTF8let matches1 : Array (Nat × Nat) := Id.run dolet mut acc : Array (Nat × Nat) := #[]for row in matchingRows dolet lineMatches := collectMatchesInLine buf.table row oldBytesif doGlobal thenacc := acc.append lineMatcheselsematch lineMatches[0]? with| some first => acc := acc.push first| none => pure ()return acclet newTable := buf.table.applyReplacements cursorOffset matches1 newlet newBuf := { buf with table := newTable, dirty := true }state.updateActiveBuffer (fun _ => newBuf)else{ state with message := s!"Unsupported global subcommand: {subcmd}" }def execSubstitute (cmd : String) (state : EditorState) : EditorState :=match parseSubstitute cmd with| none => { state with message := s!"Invalid substitute: {cmd}" }| some (isGlobal, old, new, flags) =>if old.isEmpty then{ state with message := "Empty substitute pattern" }elselet doGlobal := flags.contains 'g'let buf := state.getActiveBufferlet cursor := state.getCursorlet cursorOffset := ViE.getOffsetFromPointInBuffer buf cursor.row.val cursor.col.val |>.getD 0let patBytes := old.toUTF8let matches1 :=if isGlobal thenif doGlobal thencollectMatchesInPieceTable buf.table patByteselseId.run dolet lineCount := buf.lineCountlet mut acc : Array (Nat × Nat) := #[]for row in [0:lineCount] domatch buf.table.getLineRange row with| some (startOff, len) =>let bytes := ViE.PieceTree.getBytes buf.table.tree startOff len buf.tablematch (collectMatchesInBytes bytes patBytes)[0]? with| some (s, e) => acc := acc.push (startOff + s, startOff + e)| none => pure ()| none => pure ()return accelsematch buf.table.getLineRange cursor.row.val with| some (startOff, len) =>let bytes := ViE.PieceTree.getBytes buf.table.tree startOff len buf.tablelet localMatches := collectMatchesInBytes bytes patByteslocalMatches.map (fun (s, e) => (startOff + s, startOff + e))| none => #[]let matches2 :=if doGlobal || isGlobal thenmatches1elsematch matches1[0]? with| some first => #[first]| none => #[]let newTable := buf.table.applyReplacements cursorOffset matches2 newlet newBuf := { buf with table := newTable, dirty := true }state.updateActiveBuffer (fun _ => newBuf)
let s_indent ← runKeys s0 ([Key.char 'i'] ++ keys " indented\nx" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char 'y', Key.char 'y', Key.char 'j', Key.char 'p'])assertCursor "linewise paste moves to first non-blank" s_indent 2 2-- paste should not overwrite registerlet s_reg0 ← runKeys s0 ([Key.char 'i'] ++ keys "one\ntwo" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char 'y', Key.char 'y'])let regBefore := s_reg0.clipboardlet s_regP ← runKeys s_reg0 [Key.char 'j', Key.char 'p']match (regBefore, s_regP.clipboard) with| (some before, some after) =>assertEqual "paste keeps register kind" before.kind after.kindassertEqual "paste keeps register text" before.text after.text| _ => assertEqual "paste keeps register" true false
-- charwise y/p from normal modelet s_char0 ← runKeys s0 ([Key.char 'i'] ++ keys "hello" ++ [Key.esc] ++ [Key.char '0'])let s_charY ← runKeys s_char0 [Key.char 'v', Key.char 'l', Key.char 'y']let s_charP ← runKeys s_charY [Key.char '$', Key.char 'p']assertBuffer "charwise paste in normal mode" s_charP "hellohe"assertCursor "charwise paste cursor at end" s_charP 0 6let s_charP2 ← runKeys s_charY [Key.char '0', Key.char 'P']assertBuffer "charwise P pastes before cursor" s_charP2 "hehello"assertCursor "charwise P cursor at end" s_charP2 0 1
assertBuffer "visual y yanks selection" s_vyp "highlight me\nhighlight"
assertBuffer "visual y yanks selection" s_vyp "highlight mehighlight"let s_char0 ← runKeys s0 ([Key.char 'i'] ++ keys "abc" ++ [Key.esc] ++ [Key.char '0'])let s_charY ← runKeys s_char0 [Key.char 'l', Key.char 'v', Key.char 'y']let s_charP ← runKeys s_charY [Key.char '$', Key.char 'p']assertBuffer "charwise paste appends" s_charP "abcb"assertCursor "charwise paste cursor at end" s_charP 0 3let s_charP2 ← runKeys s_charY [Key.char '0', Key.char 'P']assertBuffer "charwise P inserts before" s_charP2 "babc"assertCursor "charwise P cursor at end" s_charP2 0 0-- visual block yank/paste cursor positionlet s_blk0 ← runKeys s0 ([Key.char 'i'] ++ keys "abcd\nefgh" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char '0'])let s_blkY ← runKeys s_blk0 [Key.char 'l', Key.char 'V', Key.char 'l', Key.char 'j', Key.char 'y']let s_blkP ← runKeys s_blkY [Key.char 'g', Key.char 'g', Key.char '0', Key.char 'p']assertBuffer "visual block y/p inserts block" s_blkP "abcbcd\nefgfgh"assertCursor "visual block paste cursor at block start" s_blkP 0 1let s_blkP2 ← runKeys s_blkY [Key.char 'g', Key.char 'g', Key.char '0', Key.char 'P']assertBuffer "visual block P inserts block" s_blkP2 "bcabcd\nfgefgh"assertCursor "visual block P cursor at block start" s_blkP2 0 0let s_blkD0 ← runKeys s0 ([Key.char 'i'] ++ keys "abcd\nefgh" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g', Key.char '0'])let s_blkD ← runKeys s_blkD0 [Key.char 'l', Key.char 'V', Key.char 'l', Key.char 'j', Key.char 'd']assertBuffer "visual block d deletes block" s_blkD "ad\neh"match s_blkD.clipboard with| some reg =>assertEqual "visual block d register kind" RegisterKind.blockwise reg.kindassertEqual "visual block d register text" "bc\nfg" reg.text| none => assertEqual "visual block d register set" true false-- linewise yank/paste (via yy + P)let s_line0 ← runKeys s0 ([Key.char 'i'] ++ keys "aa\nbb\ncc" ++ [Key.esc] ++ [Key.char 'g', Key.char 'g'])let s_lineY ← runKeys s_line0 [Key.char 'y', Key.char 'y']let s_lineP ← runKeys s_lineY [Key.char 'j', Key.char 'P']assertBuffer "linewise paste above keeps lines" s_lineP "aa\naa\nbb\ncc"
def testSearch : IO Unit := doIO.println " Testing Search..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "hello world\nhello again\n" ++ [Key.esc])let s2 ← runKeys s1 ([Key.char '/'] ++ keys "hello" ++ [Key.enter])assertCursor "/hello finds first match" s2 0 0let s3 ← runKeys s2 [Key.char 'n']assertCursor "n finds next match" s3 1 0let s4 ← runKeys s3 [Key.char 'N']assertCursor "N finds previous match" s4 0 0let s5 ← runKeys s4 ([Key.char '?'] ++ keys "world" ++ [Key.enter])assertCursor "?world searches backward" s5 0 6def testCommandSubstitute : IO Unit := doIO.println " Testing Command Substitute..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "foo bar\nfoo baz\nbar foo\n" ++ [Key.esc] ++ keys "gg0")let s2 ← runKeys s1 ([Key.char ':'] ++ keys "s/foo/xxx/" ++ [Key.enter])assertBuffer ":s replaces first match on current line" s2 "xxx bar\nfoo baz\nbar foo\n"let s3 := ViE.initialStatelet s4 ← runKeys s3 ([Key.char 'i'] ++ keys "foo foo\nfoo foo\n" ++ [Key.esc] ++ keys "gg0")let s5 ← runKeys s4 ([Key.char ':'] ++ keys "%s/foo/yyy/" ++ [Key.enter])assertBuffer ":%s replaces first match per line" s5 "yyy foo\nyyy foo\n"let s6 := ViE.initialStatelet s7 ← runKeys s6 ([Key.char 'i'] ++ keys "foo bar\nfoo baz\nbar foo\n" ++ [Key.esc] ++ keys "gg0")let s8 ← runKeys s7 ([Key.char ':'] ++ keys "%s/foo/yyy/g" ++ [Key.enter])assertBuffer ":%s with g replaces all matches" s8 "yyy bar\nyyy baz\nbar yyy\n"
def testCommandGlobal : IO Unit := doIO.println " Testing Command Global..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "a\nfoo1\nb\nfoo2\n" ++ [Key.esc] ++ keys "gg0")let s2 ← runKeys s1 ([Key.char ':'] ++ keys "g/foo/ d" ++ [Key.enter])assertBuffer ":g/pat/ d deletes matching lines" s2 "a\nb\n"let s3 := ViE.initialStatelet s4 ← runKeys s3 ([Key.char 'i'] ++ keys "foo foo\nbar foo\nfoo bar\n" ++ [Key.esc] ++ keys "gg0")let s5 ← runKeys s4 ([Key.char ':'] ++ keys "g/foo/ s/foo/xxx/" ++ [Key.enter])assertBuffer ":g/pat/ s replaces first match per line" s5 "xxx foo\nbar xxx\nxxx bar\n"let s6 := ViE.initialStatelet s7 ← runKeys s6 ([Key.char 'i'] ++ keys "keep1\nfoo\nkeep2\n" ++ [Key.esc] ++ keys "gg0")let s8 ← runKeys s7 ([Key.char ':'] ++ keys "v/foo/ d" ++ [Key.enter])assertBuffer ":v/pat/ d deletes non-matching lines" s8 "foo\n"def testCommandBloom : IO Unit := doIO.println " Testing Command Bloom..."let s0 := ViE.initialStatelet s1 ← runKeys s0 ([Key.char 'i'] ++ keys "hello bloom\nbloom hello\n" ++ [Key.esc] ++ keys "gg0")let s2 ← runKeys s1 ([Key.char ':'] ++ keys "bloom /bloom" ++ [Key.enter])assertCursor ":bloom moves to first match" s2 0 6let s3 ← runKeys s2 ([Key.char ':'] ++ keys "bloom /nomatch" ++ [Key.enter])assertEqual ":bloom not found message" "Pattern not found: nomatch" s3.message