ZL7ZSOEOGP2E24UEFC5VVPN5GTL3EUL34FA7F47WWWFPHJH2RS2AC 25KGF2W2ORVH3Z7RIBDBRKILMM624MNHIMN5QXNMZOWQ5DOJUCZAC NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC 6W6OJAUT3KLOXXKYR4GA3MG4ACLO2T4KX3SGD2KZDX6MYEZYTPHAC TKAAHADV62OQORAO7MYRRRHTGPMG3GKXU4Z4MFNLAO6DLTSDU3CAC CNJGJCJZ6LRHHIRSRATSE3D3Z5OQGSSTDMXCPVXSKRQLYJFME6IAC WRBKZMYVNHRWT7TTUGTDJ3TMWZB32QYW5PCLKTTVAJ2YF6OI3LTAC 32SDOYNGPOAAMEQMZLZUE3XE6D5CFSZU6M3JDRERUVPAB4TLZOOAC 5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC KJLCU4X5Z3CZM4AORMWIKOPBWPVTDMLK4LYH7UXBJFUGL7AUQCSQC U45XPF3YKPXXRJ4MN24T2RV7GOL4FZKQSWX5P5I7WT4HC5XF4FHAC DTAIE7PK6TZLNSBQGENS6RT7FFOTMAPSE6ZTPDADINGJF5NTHLWQC GUD2J453E3UTRJZIEEUUJ3ZIGL72ETUXTO57XQIZ2Y3ZU3C2R55QC SEIYD7YXZ5XI4W7UVF5O2UFLA6OCZZCOLV2XB46RKJ5EN6UQC4UAC elseaccelseacctermination_by s.bsize - i.1loop 0 0 ""/-- Normalize invalid tab stop values.Tab stop 0 would break modulo logic, so clamp to 1. -/def normalizeTabStop (tabStop : Nat) : Nat :=if tabStop == 0 then 1 else tabStop/-- Display width contribution of a tab at a given display column. -/def tabWidthAt (tabStop : Nat) (col : Nat) : Nat :=let ts := normalizeTabStop tabStoplet rem := col % tsif rem == 0 then ts else ts - rem/-- Character width with tab-stop awareness. -/def charWidthAt (tabStop : Nat) (col : Nat) (c : Char) : Nat :=if c == '\t' thentabWidthAt tabStop colelsecharWidth c/-- Display text for a character with tab-stop awareness. -/def getDisplayStringAt (tabStop : Nat) (col : Nat) (c : Char) : String :=if c == '\t' then"".pushn ' ' (tabWidthAt tabStop col)elsegetDisplayString c/-- Calculate the total visual width of a string with tab-stop awareness. -/def stringWidthWithTabStop (s : String) (tabStop : Nat) : Nat :=let rec loop (cs : List Char) (acc : Nat) : Nat :=match cs with| [] => acc| c :: rest =>let w := charWidthAt tabStop acc cloop rest (acc + w)loop s.toList 0/-- Calculate the total visual width of a substring with tab-stop awareness. -/def substringWidthWithTabStop (s : Substring.Raw) (tabStop : Nat) : Nat :=let rec loop (i : String.Pos.Raw) (acc : Nat) : Nat :=if h : i.byteIdx < s.bsize thenlet c := s.get ilet i' := s.next ihave := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)let w := charWidthAt tabStop acc cloop i' (acc + w)elseacctermination_by s.bsize - i.1loop 0 0/-- Convert a display column to a character index (0-based), tab-stop aware. -/def displayColToCharIndexWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=let rec loop (cs : List Char) (idx width : Nat) : Nat :=match cs with| [] => idx| c :: rest =>let w := charWidthAt tabStop width cif width + w > col thenidxelseloop rest (idx + 1) (width + w)loop s.toList 0 0/-- Display width of the first `idx` characters in a string, tab-stop aware. -/def displayWidthAtCharIndexWithTabStop (s : String) (tabStop : Nat) (idx : Nat) : Nat :=let rec loop (cs : List Char) (i acc : Nat) : Nat :=match cs with| [] => acc| c :: rest =>if i >= idx thenaccelselet w := charWidthAt tabStop acc cloop rest (i + 1) (acc + w)loop s.toList 0 0/-- Convert a display column to a UTF-8 byte offset within a string, tab-stop aware. -/def displayColToByteOffsetWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=let rec loop (cs : List Char) (byteAcc widthAcc : Nat) : Nat :=match cs with| [] => byteAcc| c :: rest =>let w := charWidthAt tabStop widthAcc clet b := c.toString.toUTF8.sizeif widthAcc + w > col thenbyteAccelseloop rest (byteAcc + b) (widthAcc + w)loop s.toList 0 0/-- Build display-column to byte-offset index with tab-stop awareness. -/def buildDisplayByteIndexWithTabStop (s : String) (tabStop : Nat) : Array (Nat × Nat) :=let rec loop (cs : List Char) (disp bytes : Nat) (acc : Array (Nat × Nat)) : Array (Nat × Nat) :=match cs with| [] => acc| c :: rest =>let w := charWidthAt tabStop disp clet b := c.toString.toUTF8.sizelet disp' := disp + wlet bytes' := bytes + bloop rest disp' bytes' (acc.push (disp', bytes'))loop s.toList 0 0 #[(0, 0)]/-- Compute next display column (one character advance), tab-stop aware. -/def nextDisplayColWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=let idx := displayColToCharIndexWithTabStop s tabStop collet startWidth := displayWidthAtCharIndexWithTabStop s tabStop idxif col < startWidth thenstartWidthelselet chars := s.toListif idx < chars.length thenlet w := charWidthAt tabStop startWidth (chars[idx]!)startWidth + welsecol/-- Compute previous display column (one character back), tab-stop aware. -/def prevDisplayColWithTabStop (s : String) (tabStop : Nat) (col : Nat) : Nat :=if col == 0 then0elselet idx := displayColToCharIndexWithTabStop s tabStop collet startWidth := displayWidthAtCharIndexWithTabStop s tabStop idxif col > startWidth thenstartWidthelse if idx == 0 then0elsedisplayWidthAtCharIndexWithTabStop s tabStop (idx - 1)/-- Drop `width` display columns from substring start, tab-stop aware. -/def dropByDisplayWidthWithTabStop (s : Substring.Raw) (tabStop : Nat) (width : Nat) : Substring.Raw :=let rec loop (i : String.Pos.Raw) (acc : Nat) : Substring.Raw :=if h : i.byteIdx < s.bsize thenlet c := s.get ilet w := charWidthAt tabStop acc cif acc + w > width thens.extract i ⟨s.bsize⟩elselet i' := s.next ihave := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)loop i' (acc + w)elses.extract i ⟨s.bsize⟩termination_by s.bsize - i.1loop 0 0/-- Take characters from substring until visual width limit, tab-stop aware. -/def takeByDisplayWidthWithTabStop (s : Substring.Raw) (tabStop : Nat) (width : Nat) : String :=let rec loop (i : String.Pos.Raw) (currW : Nat) (acc : String) : String :=if h : i.byteIdx < s.bsize thenlet c := s.get ilet w := charWidthAt tabStop currW cif currW + w <= width thenlet i' := s.next ihave := Nat.sub_lt_sub_left h (Substring.Raw.lt_next s i h)loop i' (currW + w) (acc ++ getDisplayStringAt tabStop currW c)
let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.vallet dl := takeVisual sub availableWidth
let sub := ViE.Unicode.dropByDisplayWidthWithTabStop lineStr.toRawSubstring state.config.tabStop view.scrollCol.vallet dl := ViE.Unicode.takeByDisplayWidthWithTabStop sub state.config.tabStop availableWidth
let sub := ViE.Unicode.dropByDisplayWidth lineStr.toRawSubstring view.scrollCol.vallet dl := takeVisual sub availableWidth
let sub := ViE.Unicode.dropByDisplayWidthWithTabStop lineStr.toRawSubstring state.config.tabStop view.scrollCol.vallet dl := ViE.Unicode.takeByDisplayWidthWithTabStop sub state.config.tabStop availableWidth
let sub := ViE.Unicode.dropByDisplayWidth raw.toRawSubstring view.scrollCol.vallet plainShown := takeVisual sub textWlet shownW := Unicode.stringWidth plainShown
let sub := ViE.Unicode.dropByDisplayWidthWithTabStop raw.toRawSubstring st.config.tabStop view.scrollCol.vallet plainShown := ViE.Unicode.takeByDisplayWidthWithTabStop sub st.config.tabStop textWlet shownW := Unicode.stringWidthWithTabStop plainShown st.config.tabStop
def computeFloatingOverlayLayout (rows cols : Nat) (overlay : FloatingOverlay) : Option FloatingOverlayLayout := Id.run do
def computeFloatingOverlayLayout (rows cols : Nat) (tabStop : Nat) (overlay : FloatingOverlay) : Option FloatingOverlayLayout := Id.run do
let naturalWidthContent := lines.foldl (fun acc ln => max acc (Unicode.stringWidth ln)) 0let naturalWidth := max naturalWidthContent (Unicode.stringWidth titleText)
let naturalWidthContent := lines.foldl (fun acc ln => max acc (Unicode.stringWidthWithTabStop ln tabStop)) 0let naturalWidth := max naturalWidthContent (Unicode.stringWidthWithTabStop titleText tabStop)
def renderFloatingOverlay (rows cols : Nat) (overlay : FloatingOverlay) : Array String := Id.run dolet some layout := computeFloatingOverlayLayout rows cols overlay | return #[]
def renderFloatingOverlay (rows cols : Nat) (tabStop : Nat) (overlay : FloatingOverlay) : Array String := Id.run dolet some layout := computeFloatingOverlayLayout rows cols tabStop overlay | return #[]
let clippedTitle := Unicode.takeByDisplayWidth titleText.toRawSubstring innerWidthout := out.push s!"| {rightPadVisual clippedTitle innerWidth} |"
let clippedTitle := Unicode.takeByDisplayWidthWithTabStop titleText.toRawSubstring tabStop innerWidthlet titleW := Unicode.stringWidthWithTabStop clippedTitle tabStoplet titlePad := if titleW < innerWidth then "".pushn ' ' (innerWidth - titleW) else ""out := out.push s!"| {clippedTitle}{titlePad} |"
let clipped := Unicode.takeByDisplayWidth raw.toRawSubstring innerWidth
let clipped := Unicode.takeByDisplayWidthWithTabStop raw.toRawSubstring tabStop innerWidthlet clippedW := Unicode.stringWidthWithTabStop clipped tabStoplet pad := if clippedW < innerWidth then "".pushn ' ' (innerWidth - clippedW) else ""
def lineDisplayWidth (buffer : FileBuffer) (row : Row) : Nat :=ViE.getLineLengthFromBuffer buffer row |>.getD 0
def lineDisplayWidth (tabStop : Nat) (buffer : FileBuffer) (row : Row) : Nat :=ViE.getLineLengthFromBufferWithTabStop buffer row tabStop |>.getD 0
def charAtDisplayCol (lineStr : String) (col : Col) : Char :=let idx := ViE.Unicode.displayColToCharIndex lineStr col.val
def charAtDisplayCol (tabStop : Nat) (lineStr : String) (col : Col) : Char :=let idx := ViE.Unicode.displayColToCharIndexWithTabStop lineStr tabStop col.val
def findNextWordEndForwardCore (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) (fuel : Nat) : Row × Col :=
def findNextWordEndForwardCore (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) (fuel : Nat) : Row × Col :=
def findNextForward (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) : Row × Col :=findNextForwardCore buffer row col started (wordMoveFuel buffer)
def findNextForward (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (started : Bool) : Row × Col :=findNextForwardCore tabStop buffer row col started (wordMoveFuel buffer)
def findNextWordEndForward (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) : Row × Col :=findNextWordEndForwardCore buffer row col wasTv (wordMoveFuel buffer)
def findNextWordEndForward (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wasTv : Bool) : Row × Col :=findNextWordEndForwardCore tabStop buffer row col wasTv (wordMoveFuel buffer)
let prevLen := lineDisplayWidth buffer prevRowif prevLen > 0 then findPrevStartCore buffer prevRow ⟨prevLen - 1⟩ fuel else (prevRow, 0)
let prevLen := lineDisplayWidth tabStop buffer prevRowif prevLen > 0 then findPrevStartCore tabStop buffer prevRow ⟨prevLen - 1⟩ fuel else (prevRow, 0)
def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=findPrevStartCore buffer row col (wordMoveFuel buffer)
def findPrevStart (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=findPrevStartCore tabStop buffer row col (wordMoveFuel buffer)
def consumeWordBackward (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=consumeWordBackwardCore buffer row col wantKw (wordMoveFuel buffer)
def consumeWordBackward (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=consumeWordBackwardCore tabStop buffer row col wantKw (wordMoveFuel buffer)
def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=findNextEndCore buffer row col (wordMoveFuel buffer)
def findNextEnd (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=findNextEndCore tabStop buffer row col (wordMoveFuel buffer)
def consumeWordToEnd (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=consumeWordToEndCore buffer row col wantKw (wordMoveFuel buffer)
def consumeWordToEnd (tabStop : Nat) (buffer : FileBuffer) (row : Row) (col : Col) (wantKw : Bool) : Row × Col :=consumeWordToEndCore tabStop buffer row col wantKw (wordMoveFuel buffer)
match ViE.getOffsetFromPointInBuffer buffer cursor.row.val prevC.val,ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with
match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val prevC.val tabStop,ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop with
match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with
match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop,ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val nextC.val tabStop with
match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with
match ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val cursor.col.val tabStop,ViE.getOffsetFromPointInBufferWithTabStop buffer cursor.row.val nextC.val tabStop with
match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with
match ViE.getOffsetFromPointInBufferWithTabStop buffer p1.row.val p1.col.val tabStop,ViE.getOffsetFromPointInBufferWithTabStop buffer p2.row.val p2.col.val tabStop with
private def PieceTable.findLineForOffsetCore (pt : PieceTable) (target : Nat) (low high : Nat) (fuel : Nat) : Option (Nat × Nat) :=match fuel with| 0 => none| fuel + 1 =>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.findLineForOffsetCore pt target low (mid - 1) fuelelsePieceTable.findLineForOffsetCore pt target (mid + 1) high fuel| none => none
private def PieceTable.findLineForOffsetCore (pt : PieceTable) (target : Nat) (low highExcl : Nat) : Option (Nat × Nat) :=if low >= highExcl then noneelselet mid := low + (highExcl - low) / 2match pt.getLineRange mid with| some (start, len) =>let endOff := start + lenif target >= start && target <= endOff thensome (mid, target - start)else if target < start thenPieceTable.findLineForOffsetCore pt target low midelsePieceTable.findLineForOffsetCore pt target (mid + 1) highExcl| none => nonetermination_by highExcl - lowdecreasing_by· simp_wfomega· simp_wfomega
private def concatCore (l : ViE.PieceTree) (r : ViE.PieceTree) (pt : ViE.PieceTable) (fuel : Nat) : ViE.PieceTree :=match fuel with| 0 =>-- Rebuild into a balanced tree in pathological cases instead of creating deep chains.fromPieces (toPieces l ++ toPieces r) pt| fuel + 1 =>match l, r with| ViE.PieceTree.empty, _ => r| _, ViE.PieceTree.empty => l| ViE.PieceTree.leaf ps1 _ _, ViE.PieceTree.leaf ps2 _ _ =>-- Try to merge the last piece of ps1 with the first piece of ps2
private def concatCore (l : ViE.PieceTree) (r : ViE.PieceTree) (pt : ViE.PieceTable) : ViE.PieceTree :=match l, r with| ViE.PieceTree.empty, _ => r| _, ViE.PieceTree.empty => l| ViE.PieceTree.leaf ps1 _ _, ViE.PieceTree.leaf ps2 _ _ =>-- Fast path for adjacent leaves; preserve piece merging behavior.
else if ps1.size > 0 then lelse r| ViE.PieceTree.internal cs1 _ _, ViE.PieceTree.internal cs2 _ _ =>let h1 := height llet h2 := height rif h1 == h2 then-- Merge boundary childrenlet lastChild := cs1.back!let firstChild := cs2[0]!let merged := concatCore lastChild firstChild pt fuelmatch merged with| ViE.PieceTree.internal newCS s _ =>if s.height == h1 then-- newCS is at the same level as siblingslet combined := (cs1.pop) ++ newCS ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]else-- height did not increase, just one childlet combined := (cs1.pop).push merged ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]| _ =>let combined := (cs1.pop).push merged ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]else if h1 > h2 then-- Insert r into l's right sidelet lastChild := cs1.back!let newLast := concatCore lastChild r pt fuelmatch newLast with| ViE.PieceTree.internal newChildren s _ =>if s.height == h1 then-- Split happened at l's levellet combined := (cs1.pop) ++ newChildrenif combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]elsemkInternal ((cs1.pop).push newLast)| _ => mkInternal ((cs1.pop).push newLast)
else if ps1.size > 0 thenl
-- Insert l into r's left sidelet firstChild := cs2[0]!let newFirst := concatCore l firstChild pt fuelmatch newFirst with| ViE.PieceTree.internal newChildren s _ =>if s.height == h2 thenlet combined := newChildren ++ (cs2.extract 1 cs2.size)if combined.size <= ViE.NodeCapacity then mkInternal combinedelselet mid := combined.size / 2mkInternal #[mkInternal (combined.extract 0 mid), mkInternal (combined.extract mid combined.size)]elsemkInternal (#[newFirst] ++ (cs2.extract 1 cs2.size))| _ => mkInternal (#[newFirst] ++ (cs2.extract 1 cs2.size))-- Mixed types: wrap the smaller one and recurse| ViE.PieceTree.leaf .. , ViE.PieceTree.internal .. => concatCore (mkInternal #[l]) r pt fuel| ViE.PieceTree.internal .. , ViE.PieceTree.leaf .. => concatCore l (mkInternal #[r]) pt fueltermination_by fueldecreasing_byall_goals exact Nat.lt_succ_self _
r| _, _ =>-- For mixed or internal trees, rebuild a balanced tree from in-order pieces.fromPieces (toPieces l ++ toPieces r) pt
private def splitCore (t : ViE.PieceTree) (offset : Nat) (pt : ViE.PieceTable) (fuel : Nat) : (ViE.PieceTree × ViE.PieceTree) :=match fuel with| 0 => (t, ViE.PieceTree.empty)| fuel + 1 =>match t with| ViE.PieceTree.empty => (ViE.PieceTree.empty, ViE.PieceTree.empty)
private def splitCore (t : ViE.PieceTree) (offset : Nat) (pt : ViE.PieceTable) : (ViE.PieceTree × ViE.PieceTree) :=Id.run doif offset == 0 thenreturn (ViE.PieceTree.empty, t)let mut node := tlet mut off := offsetlet mut frames : Array (Array ViE.PieceTree × Array ViE.PieceTree) := #[]while true domatch node with| ViE.PieceTree.empty =>return (ViE.PieceTree.empty, ViE.PieceTree.empty)
Id.run dolet mut i := 0let mut accOffset := 0while i < pieces.size dolet p := pieces[i]!if offset < accOffset + p.length thenlet relOffset := offset - accOffsetif relOffset == 0 thenreturn (mkLeaf (pieces.extract 0 i) pt, mkLeaf (pieces.extract i pieces.size) pt)
let mut i := 0let mut accOffset := 0let mut leftTree := nodelet mut rightTree := ViE.PieceTree.emptylet mut found := falsewhile i < pieces.size && !found dolet p := pieces[i]!if off < accOffset + p.length thenlet relOffset := off - accOffsetif relOffset == 0 thenleftTree := mkLeaf (pieces.extract 0 i) ptrightTree := mkLeaf (pieces.extract i pieces.size) ptelse
return (mkLeaf ((pieces.extract 0 i).push p1) pt, mkLeaf (#[p2] ++ (pieces.extract (i + 1) pieces.size)) pt)
leftTree := mkLeaf ((pieces.extract 0 i).push p1) ptrightTree := mkLeaf (#[p2] ++ (pieces.extract (i + 1) pieces.size)) ptfound := trueelse
return (t, ViE.PieceTree.empty)
if !found thenleftTree := noderightTree := ViE.PieceTree.emptylet mut l := leftTreelet mut r := rightTreelet mut fi := frames.sizewhile fi > 0 dolet j := fi - 1let (leftSibs, rightSibs) := frames[j]!l := mkInternal (leftSibs.push l)r := mkInternal (#[r] ++ rightSibs)fi := jreturn (l, r)
Id.run dolet mut i := 0let mut accOffset := 0while i < children.size dolet c := children[i]!let cLen := length cif offset < accOffset + cLen thenlet (l, r) := splitCore c (offset - accOffset) pt fuellet leftSide := mkInternal ((children.extract 0 i).push l)let rightSide := mkInternal (#[r] ++ (children.extract (i + 1) children.size))return (leftSide, rightSide)
let mut i := 0let mut accOffset := 0let mut found := falsewhile i < children.size && !found dolet c := children[i]!let cLen := length cif off < accOffset + cLen thenframes := frames.push (children.extract 0 i, children.extract (i + 1) children.size)node := coff := off - accOffsetfound := trueelse
private def getBytesCore (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) (fuel : Nat) : ByteArray :=let rec collect (fuel : Nat) (t : ViE.PieceTree) (off : Nat) (l : Nat) (acc : Array ByteArray) : (Array ByteArray × Nat) :=match fuel with| 0 => (acc, 0)| fuel + 1 =>if l == 0 then (acc, 0)elsematch t with| ViE.PieceTree.empty => (acc, 0)| ViE.PieceTree.leaf pieces _ _ =>Id.run dolet mut i := 0let mut accOffset := 0let mut currAcc := acclet mut remain := lwhile i < pieces.size && remain > 0 dolet p := pieces[i]!let pLen := p.lengthif off < accOffset + pLen thenlet pStart := if off > accOffset then off - accOffset else 0let readLen := min remain (pLen - pStart)let buf := PieceTableHelper.getBuffer pt p.sourcelet slice := buf.extract (p.start + pStart) (p.start + pStart + readLen)currAcc := currAcc.push sliceremain := remain - readLenaccOffset := accOffset + pLeni := i + 1return (currAcc, l - remain)| ViE.PieceTree.internal children _ _ =>Id.run dolet mut i := 0let mut accOffset := 0let mut currAcc := acclet mut remain := lwhile i < children.size && remain > 0 dolet c := children[i]!let cLen := length cif off < accOffset + cLen thenlet cStart := if off > accOffset then off - accOffset else 0let (newAcc, readInThisChild) := collect fuel c cStart remain currAcccurrAcc := newAccremain := remain - readInThisChildaccOffset := accOffset + cLeni := i + 1return (currAcc, l - remain)let (chunks, _) := collect fuel t offset len #[]chunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])
private def getBytesCore (t : ViE.PieceTree) (offset : Nat) (len : Nat) (pt : ViE.PieceTable) : ByteArray :=if len == 0 thenByteArray.mk #[]elselet endOffset := offset + lenlet chunks := Id.run dolet mut stack : List (ViE.PieceTree × Nat) := [(t, 0)]let mut out : Array ByteArray := #[]let mut cursor := offsetlet mut remain := lenwhile remain > 0 && !stack.isEmpty domatch stack with| [] => pure ()| (node, baseOffset) :: rest =>stack := restlet nodeLen := length nodelet nodeEnd := baseOffset + nodeLenif nodeEnd <= cursor || baseOffset >= endOffset thenpure ()elsematch node with| ViE.PieceTree.empty => pure ()| ViE.PieceTree.leaf pieces _ _ =>let mut i := 0let mut pieceBase := baseOffsetwhile i < pieces.size && remain > 0 dolet p := pieces[i]!let pStart := pieceBaselet pEnd := pieceBase + p.lengthif pEnd > cursor && pStart < endOffset thenlet startInPiece := if cursor > pStart then cursor - pStart else 0let maxReadable := p.length - startInPiecelet untilEnd := endOffset - (pStart + startInPiece)let readLen := min remain (min maxReadable untilEnd)if readLen > 0 thenlet buf := PieceTableHelper.getBuffer pt p.sourcelet slice := buf.extract (p.start + startInPiece) (p.start + startInPiece + readLen)out := out.push slicecursor := cursor + readLenremain := remain - readLenpieceBase := pieceBase + p.lengthi := i + 1| ViE.PieceTree.internal children _ _ =>let mut i := children.sizelet mut childEnd := nodeEndwhile i > 0 dolet j := i - 1let child := children[j]!let childLen := length childlet childStart := childEnd - childLenif childEnd > cursor && childStart < endOffset thenstack := (child, childStart) :: stackchildEnd := childStarti := jreturn outchunks.foldl (fun (acc : ByteArray) (b : ByteArray) => acc ++ b) (ByteArray.mk #[])
Id.run dolet mut i := 0let mut currN := nlet mut currOff := accOffsetwhile i < pieces.size dolet p := pieces[i]!if currN < p.lineBreaks thenlet buf := PieceTableHelper.getBuffer pt p.sourcelet mut j := 0let mut targetN := currNlet mut relOffset := p.lengthlet mut done := falsewhile j < p.length && !done doif buf[p.start + j]! == 10 thenif targetN == 0 thenrelOffset := j + 1done := trueelsetargetN := targetN - 1j := j + 1return some (p, currOff, relOffset)currN := currN - p.lineBreakscurrOff := currOff + p.lengthi := i + 1return none
let mut i := 0while i < pieces.size dolet p := pieces[i]!if currN < p.lineBreaks thenlet buf := PieceTableHelper.getBuffer pt p.sourcelet mut j := 0let mut targetN := currNlet mut relOffset := p.lengthlet mut done := falsewhile j < p.length && !done doif buf[p.start + j]! == 10 thenif targetN == 0 thenrelOffset := j + 1done := trueelsetargetN := targetN - 1j := j + 1return some (p, currOff, relOffset)currN := currN - p.lineBreakscurrOff := currOff + p.lengthi := i + 1return none
Id.run dolet mut i := 0let mut currN := nlet mut currOff := accOffsetwhile i < children.size dolet child := children[i]!let childLines := lineBreaks childif currN < childLines thenreturn findNthNewlineLeafCore child currN pt currOff fuel
let mut i := 0let mut found := falsewhile i < children.size && !found dolet child := children[i]!let childLines := lineBreaks childif currN < childLines thennode := childfound := trueelse
private def maximalSuffixLoopCore (x : ByteArray) (useLe : Bool) (m ms j k p : Int) (fuel : Nat) : (Int × Int) :=match fuel with| 0 => (ms, p)| fuel + 1 =>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 thenmaximalSuffixLoopCore x useLe m ms (j + k) 1 (j + k - ms) fuelelse if a == b thenif k != p thenmaximalSuffixLoopCore x useLe m ms j (k + 1) p fuelelsemaximalSuffixLoopCore x useLe m ms (j + p) 1 p fuel
def maximalSuffixLoop (x : ByteArray) (useLe : Bool) (m ms j k p : Int) : (Int × Int) :=Id.run dolet mut ms := mslet mut j := jlet mut k := klet mut p := p-- Keep an execution cap for robustness against malformed index states.let mNat := Int.toNat mlet mut steps := (mNat + 1) * (mNat + 1) + 1while steps > 0 && j + k < m dolet a := x[Int.toNat (j + k)]!let b := x[Int.toNat (ms + k)]!if useLe thenif a < b thenlet jk := j + kj := jkk := 1p := jk - mselse if a == b thenif k != p thenk := k + 1
if a > b thenmaximalSuffixLoopCore x useLe m ms (j + k) 1 (j + k - ms) fuelelse if a == b thenif k != p thenmaximalSuffixLoopCore x useLe m ms j (k + 1) p fuelelsemaximalSuffixLoopCore x useLe m ms (j + p) 1 p fuelelsemaximalSuffixLoopCore x useLe m j (j + 1) 1 1 fueltermination_by fueldecreasing_byall_goals exact Nat.lt_succ_self _def maximalSuffixLoop (x : ByteArray) (useLe : Bool) (m ms j k p : Int) : (Int × Int) :=let mNat := Int.toNat mlet fuel := (mNat + 1) * (mNat + 1) + 1maximalSuffixLoopCore x useLe m ms j k p fuel
ms := jj := j + 1k := 1p := 1else if a > b thenlet jk := j + kj := jkk := 1p := jk - mselse if a == b thenif k != p thenk := k + 1elsej := j + pk := 1elsems := jj := j + 1k := 1p := 1steps := steps - 1return (ms, p)
private def twoWayForward1Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) (fuel : Nat) : Int :=match fuel with| 0 => j| fuel + 1 =>if j >= n thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayForward1Core haystack needle i n (j + 1) fuelelsejtermination_by fuel
private def twoWayForward1Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Nat) : Nat :=if j >= n thenjelse if haystack[i + j]! == needle[j]! thentwoWayForward1Core haystack needle i n (j + 1)elsejtermination_by n - j
private def twoWayBackward1Core (haystack needle : ByteArray) (i : Nat) (mem : Int) (j : Int) (fuel : Nat) : Int :=match fuel with| 0 => j| fuel + 1 =>if j <= mem thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayBackward1Core haystack needle i mem (j - 1) fuelelsejtermination_by fuel
private def twoWayBackward1Core (haystack needle : ByteArray) (i : Nat) (mem : Int) (steps : Nat) : Int :=if hSteps : steps = 0 thenmemelselet j := mem + Int.ofNat stepsif haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayBackward1Core haystack needle i mem (steps - 1)elsejtermination_by steps
private def twoWayForward2Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Int) (fuel : Nat) : Int :=match fuel with| 0 => j| fuel + 1 =>if j >= n thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayForward2Core haystack needle i n (j + 1) fuelelsejtermination_by fuel
private def twoWayForward2Core (haystack needle : ByteArray) (i : Nat) (n : Nat) (j : Nat) : Nat :=if j >= n thenjelse if haystack[i + j]! == needle[j]! thentwoWayForward2Core haystack needle i n (j + 1)elsejtermination_by n - j
private def twoWayBackward2Core (haystack needle : ByteArray) (i : Nat) (j : Int) (fuel : Nat) : Int :=match fuel with| 0 => j| fuel + 1 =>if j < 0 thenjelse if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayBackward2Core haystack needle i (j - 1) fuelelsejtermination_by fuel
private def twoWayBackward2Core (haystack needle : ByteArray) (i : Nat) (steps : Nat) : Int :=if hSteps : steps = 0 then-1elselet j := Int.ofNat steps - 1if haystack[i + Int.toNat j]! == needle[Int.toNat j]! thentwoWayBackward2Core haystack needle i (steps - 1)elsejtermination_by steps
private def twoWayShortLoopCore (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) (mem : Int) (fuel : Nat) : Option Nat :=match fuel with| 0 => none| fuel + 1 =>if i > maxStart then
private def twoWayShortLoopCore (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 + pNatif nextI <= i thennoneelselet nextMem := Int.ofNat (n - pNat - 1)twoWayShortLoopCore haystack needle _start maxStart msNat pNat n nextI nextMemelselet shift := Int.toNat (j - Int.ofNat msNat)if shift == 0 then
let 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)twoWayShortLoopCore haystack needle start maxStart msNat pNat n nextI nextMem fuel
let nextI := i + shiftif nextI <= i thennone
let shift := Int.toNat (j - Int.ofNat msNat)twoWayShortLoopCore haystack needle start maxStart msNat pNat n (i + shift) (-1) fueltermination_by fuel
twoWayShortLoopCore haystack needle _start maxStart msNat pNat n nextI (-1)termination_by maxStart + 1 - i
private def twoWayLongLoopCore (haystack needle : ByteArray) (start maxStart msNat pNat n : Nat) (i : Nat) (fuel : Nat) : Option Nat :=match fuel with| 0 => none| fuel + 1 =>if i > maxStart then
private def twoWayLongLoopCore (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 + pNatif nextI <= i thennoneelsetwoWayLongLoopCore haystack needle _start maxStart msNat pNat n nextIelselet shift := Int.toNat (j - Int.ofNat msNat)if shift == 0 then
let 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 + pNattwoWayLongLoopCore haystack needle start maxStart msNat pNat n nextI fuel
let nextI := i + shiftif nextI <= i thennone
let rec loop (i : Nat) (last : Option Nat) (fuel : Nat) : Option Nat :=match fuel with| 0 => last| fuel + 1 =>if i > maxStart then lastelsematch findPatternInBytes haystack needle i with| some idx =>if idx > maxStart then lastelse loop (idx + 1) (some idx) fuel| none => lastloop 0 none (maxStart + 1)
let 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 if idx < i then lastelse loop (idx + 1) (some idx)| none => lasttermination_by maxStart + 1 - idecreasing_bysimp_wfomegaloop 0 none
let rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (fuelN : Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=match fuelN with| 0 => (none, cache, order)| fuelN + 1 =>if baseOffset + length node <= startOffset then(none, cache, order)elsematch node with| ViE.PieceTree.empty => (none, cache, order)| ViE.PieceTree.leaf _ _ m =>let relStart := if startOffset > baseOffset then startOffset - baseOffset else 0let remain := length node - relStartlet globalStart := baseOffset + relStartlet available := total - globalStartlet readLen := min (remain + overlap) availableif readLen < pattern.size then(none, cache, order)elselet crossesBoundary := readLen > remainif !crossesBoundary && !bloomMayContain m.bits hashes then(none, cache, order)
Id.run dolet mut stack : List (ViE.PieceTree × Nat) := [(t, 0)]let mut cacheAcc := cachelet mut orderAcc := orderwhile !stack.isEmpty domatch stack with| [] => pure ()| (node, baseOffset) :: rest =>stack := restif baseOffset + length node <= startOffset thenpure ()elsematch node with| ViE.PieceTree.empty => pure ()| ViE.PieceTree.leaf _ _ m =>let relStart := if startOffset > baseOffset then startOffset - baseOffset else 0let remain := length node - relStartlet globalStart := baseOffset + relStartlet available := total - globalStartlet readLen := min (remain + overlap) availableif readLen < pattern.size thenpure ()elselet crossesBoundary := readLen > remainif !crossesBoundary && !bloomMayContain m.bits hashes thenpure ()elselet bytes := getBytes t globalStart readLen ptmatch findPatternInBytes bytes pattern 0 with| some idx => return (some (globalStart + idx), cacheAcc, orderAcc)| none => pure ()| ViE.PieceTree.internal children _ m =>if !bloomMayContain m.bits hashes thenpure ()
let bytes := getBytes t globalStart readLen ptmatch findPatternInBytes bytes pattern 0 with| some idx => (some (globalStart + idx), cache, order)| none => (none, cache, order)| ViE.PieceTree.internal children _ m =>if !bloomMayContain m.bits hashes then(none, cache, order)elseId.run dolet mut i := 0let mut offset := baseOffsetlet mut cacheAcc := cachelet mut orderAcc := orderwhile i < children.size dolet child := children[i]!
let mut i := children.sizelet mut childEnd := baseOffset + length nodewhile i > 0 dolet j := i - 1let child := children[j]!
let (res, cache', order') := searchNode child offset cacheAcc orderAcc fuelNcacheAcc := cache'orderAcc := order'match res with| some _ => return (res, cacheAcc, orderAcc)| none => pure ()offset := childEndi := i + 1return (none, cacheAcc, orderAcc)searchNode t 0 cache order fuel
stack := (child, childStart) :: stackchildEnd := childStarti := jreturn (none, cacheAcc, orderAcc)
let fuel := (height t + 4) * 32 + 64searchNextCore t pt pattern startOffset chunkSize useBloom cache order cacheMax fuel
searchNextCore t pt pattern startOffset chunkSize useBloom cache order cacheMax
let rec searchNode (node : ViE.PieceTree) (baseOffset : Nat)(cache : Lean.RBMap Nat ByteArray compare) (order : Array Nat) (fuelN : Nat): (Option Nat × Lean.RBMap Nat ByteArray compare × Array Nat) :=match fuelN with| 0 => (none, cache, order)| fuelN + 1 =>if baseOffset >= end0 then(none, cache, order)elsematch node with| ViE.PieceTree.empty => (none, cache, order)| ViE.PieceTree.leaf _ _ m =>let relEnd := min (end0 - baseOffset) (length node)let globalEnd := baseOffset + relEndlet globalStart := if baseOffset > overlap then baseOffset - overlap else 0let readLen := globalEnd - globalStartif readLen < pattern.size then(none, cache, order)elselet crossesBoundary := globalStart < baseOffsetif !crossesBoundary && !bloomMayContain m.bits hashes then(none, cache, order)
Id.run dolet mut stack : List (ViE.PieceTree × Nat) := [(t, 0)]let mut cacheAcc := cachelet mut orderAcc := orderwhile !stack.isEmpty domatch stack with| [] => pure ()| (node, baseOffset) :: rest =>stack := restif baseOffset >= end0 thenpure ()elsematch node with| ViE.PieceTree.empty => pure ()| ViE.PieceTree.leaf _ _ m =>let relEnd := min (end0 - baseOffset) (length node)let globalEnd := baseOffset + relEndlet globalStart := if baseOffset > overlap then baseOffset - overlap else 0let readLen := globalEnd - globalStartif readLen < pattern.size thenpure ()elselet crossesBoundary := globalStart < baseOffsetif !crossesBoundary && !bloomMayContain m.bits hashes thenpure ()elselet bytes := getBytes t globalStart readLen ptmatch findLastPatternInBytes bytes pattern with| some idx =>let pos := globalStart + idxif pos < end0 thenreturn (some pos, cacheAcc, orderAcc)pure ()| none => pure ()| ViE.PieceTree.internal children _ m =>if !bloomMayContain m.bits hashes thenpure ()
let bytes := getBytes t globalStart readLen ptmatch findLastPatternInBytes bytes pattern with| some idx =>let pos := globalStart + idxif pos < end0 then (some pos, cache, order) else (none, cache, order)| none => (none, cache, order)| ViE.PieceTree.internal children _ m =>if !bloomMayContain m.bits hashes then(none, cache, order)elselet 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 accId.run do
let (res, cache', order') := searchNode child childOffset cacheAcc orderAcc fuelNcacheAcc := cache'orderAcc := order'match res with| some v =>if v < end0 thenreturn (some v, cacheAcc, orderAcc)pure ()| none => pure ()
stack := (child, childOffset) :: stackchildOffset := childOffset + length child
let fuel := (height t + 4) * 32 + 64searchPrevCore t pt pattern startExclusive chunkSize useBloom cache order cacheMax fuel
searchPrevCore t pt pattern startExclusive chunkSize useBloom cache order cacheMax
/-- Get byte offset from Row/Col (display column) using per-line index cache if available. -/def getOffsetFromPointInBuffer (buffer : FileBuffer) (row col : Nat) : Option Nat :=
/-- Get byte offset from Row/Col (display column) with configurable tab stop. -/def getOffsetFromPointInBufferWithTabStop (buffer : FileBuffer) (row col tabStop : Nat) : Option Nat :=
let byteOff := match buffer.cache.findIndex ⟨row⟩ with| some idx => ViE.Unicode.displayColToByteOffsetFromIndex idx col| none => ViE.Unicode.displayColToByteOffset line col
let byteOff := ViE.Unicode.displayColToByteOffsetWithTabStop line tabStop col
/-- Get line length from FileBuffer (delegates to PieceTable) -/def getLineLengthFromBuffer (buffer : FileBuffer) (n : Row) : Option Nat :=
/-- Get line length from FileBuffer with configurable tab stop. -/def getLineLengthFromBufferWithTabStop (buffer : FileBuffer) (n : Row) (tabStop : Nat) : Option Nat :=
/-- Get byte offset from Row/Col (display column) using default tab stop. -/def getOffsetFromPointInBuffer (buffer : FileBuffer) (row col : Nat) : Option Nat :=getOffsetFromPointInBufferWithTabStop buffer row col 4/-- Get line length from FileBuffer (delegates to PieceTable) using default tab stop. -/def getLineLengthFromBuffer (buffer : FileBuffer) (n : Row) : Option Nat :=getLineLengthFromBufferWithTabStop buffer n 4
let s_tab_insert ← runKeys s0 [Key.char 'i', Key.char '\t']assertCursor "Tab advances cursor to next tab stop in insert mode" s_tab_insert 0 4let s_tab_backspace ← runKeys s0 [Key.char 'i', Key.char '\t', Key.backspace]assertBuffer "Tab backspace deletes tab in insert mode" s_tab_backspace ""assertCursor "Tab backspace restores cursor column" s_tab_backspace 0 0
let s_tab ← runKeys s0 [Key.char 'i', Key.char '\t', Key.esc]assertBuffer "Tab inserts in insert mode" s_tab "\t"assertCursor "Esc after tab returns to tab char in normal mode" s_tab 0 0let s0_tab8 := { s0 with config := { s0.config with tabStop := 8 } }let s_tab8 ← runKeys s0_tab8 [Key.char 'i', Key.char '\t']assertCursor "Tab follows custom tabStop in insert mode" s_tab8 0 8