NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC OHL2PRHBX74FZKWZU7IR6RSXA36PDZDROVI4AHTX4SO7VQFQ5RQQC 6W6OJAUT3KLOXXKYR4GA3MG4ACLO2T4KX3SGD2KZDX6MYEZYTPHAC WRBKZMYVNHRWT7TTUGTDJ3TMWZB32QYW5PCLKTTVAJ2YF6OI3LTAC U45XPF3YKPXXRJ4MN24T2RV7GOL4FZKQSWX5P5I7WT4HC5XF4FHAC 5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC GUD2J453E3UTRJZIEEUUJ3ZIGL72ETUXTO57XQIZ2Y3ZU3C2R55QC wideRanges.any fun (start, stop) => c >= start && c <= stop
if c < 0x1100 thenfalseelselet ranges := if c <= 0xFFFF then wideRangesBmp else wideRangesSupplementallet rec loop (lo hi : Nat) : Bool :=if h : lo < hi thenlet mid := (lo + hi) / 2let (start, stop) := ranges[mid]!if c < start thenloop lo midelse if c > stop thenloop (mid + 1) hielsetrueelsefalsetermination_by hi - loloop 0 ranges.size
/-- Convert a display column to a character index (0-based).If the column is in the middle of a wide character, it snaps to that character's index. -/def displayColToCharIndex (s : String) (col : Nat) : Nat :=let rec loop (cs : List Char) (idx width : Nat) : Nat :=match cs with| [] => idx| c :: rest =>let w := charWidth 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. -/def displayWidthAtCharIndex (s : String) (idx : Nat) : Nat :=let rec loop (cs : List Char) (i acc : Nat) : Nat :=match cs with| [] => acc| c :: rest =>if i >= idx thenaccelseloop rest (i + 1) (acc + charWidth c)loop s.toList 0 0/-- Convert a display column to a UTF-8 byte offset within a string. -/def displayColToByteOffset (s : String) (col : Nat) : Nat :=let rec loop (cs : List Char) (byteAcc widthAcc : Nat) : Nat :=match cs with| [] => byteAcc| c :: rest =>let w := charWidth clet b := c.toString.toUTF8.sizeif widthAcc + w > col thenbyteAccelseloop rest (byteAcc + b) (widthAcc + w)loop s.toList 0 0/-- Build an index mapping display columns to UTF-8 byte offsets at character boundaries.The result includes the starting boundary (0,0) and the final boundary (totalWidth,totalBytes). -/def buildDisplayByteIndex (s : String) : 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 := charWidth 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)]/-- Convert a display column to a UTF-8 byte offset using a precomputed index. -/def displayColToByteOffsetFromIndex (idx : Array (Nat × Nat)) (col : Nat) : Nat :=if idx.isEmpty then0elselet rec loop (lo hi : Nat) (best : Nat) : Nat :=if h : lo < hi thenlet mid := (lo + hi) / 2let (disp, bytes) := idx[mid]!if col < disp thenloop lo mid bestelseloop (mid + 1) hi byteselsebesttermination_by hi - loloop 0 idx.size 0/-- Compute the next display column (advancing by one character). -/def nextDisplayCol (s : String) (col : Nat) : Nat :=let idx := displayColToCharIndex s collet startWidth := displayWidthAtCharIndex s idxif col < startWidth thenstartWidthelselet chars := s.toListif idx < chars.length thenlet w := charWidth (chars[idx]!)startWidth + welsecol/-- Compute the previous display column (moving back by one character). -/def prevDisplayCol (s : String) (col : Nat) : Nat :=if col == 0 then0elselet idx := displayColToCharIndex s collet startWidth := displayWidthAtCharIndex s idxif col > startWidth thenstartWidthelse if idx == 0 then0elsedisplayWidthAtCharIndex s (idx - 1)/-- Drop `width` display columns from the start of a substring. -/def dropByDisplayWidth (s : Substring.Raw) (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 := charWidth 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 is reached. -/def takeByDisplayWidth (s : Substring.Raw) (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 := charWidth 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 ++ getDisplayString c)elseaccelseacctermination_by s.bsize - i.1loop 0 0 ""
partial def takeVisual (s : Substring.Raw) (width : Nat) : String :=let rec loop (sub : Substring.Raw) (currW : Nat) (acc : String) : String :=if sub.isEmpty then accelselet c := sub.frontlet w := Unicode.charWidth cif currW + w <= width thenloop (sub.drop 1) (currW + w) (acc ++ Unicode.getDisplayString c)elseaccloop s 0 ""
def takeVisual (s : Substring.Raw) (width : Nat) : String :=Unicode.takeByDisplayWidth s width
let updatedBuf := { buf with cache := buf.cache.update lineIdx dl view.scrollCol.val availableWidth }
let cache := match cachedRaw, cachedIdx with| some raw, some idx =>if raw == lineStr thenbuf.cacheelse(buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))| _, _ =>(buf.cache.updateIndex lineIdx (ViE.Unicode.buildDisplayByteIndex lineStr))let cache := (cache.update lineIdx dl view.scrollCol.val availableWidth).updateRaw lineIdx lineStrlet updatedBuf := { buf with cache := cache }
let colVal := view.scrollCol.val + idxlet isSelected := st.isInSelection lineIdx ⟨colVal⟩
let w := Unicode.charWidth chlet colVal := view.scrollCol.val + dispIdxlet isSelected :=st.isInSelection lineIdx ⟨colVal⟩ ||(w > 1 && st.isInSelection lineIdx ⟨colVal + 1⟩)
let rIdx : Row := ⟨view.scrollRow.val + visualRow⟩if let some currentLineStr := getLineFromBuffer buf rIdx thenlet preCursor := (currentLineStr.toRawSubstring.drop view.scrollCol.val).take (view.cursor.col.val - view.scrollCol.val)let visualCol := ViE.Unicode.substringWidth preCursor
-- let rIdx : Row := ⟨view.scrollRow.val + visualRow⟩if view.cursor.col.val < view.scrollCol.val thennoneelselet visualCol := view.cursor.col.val - view.scrollCol.val
{ lineMap := c.lineMap.insert r (s, scrollCol, availableWidth) }
{ c with lineMap := c.lineMap.insert r (s, scrollCol, availableWidth) }def updateRaw (c : RenderCache) (r : Row) (s : String) : RenderCache :={ c with rawLineMap := c.rawLineMap.insert r s }def updateIndex (c : RenderCache) (r : Row) (idx : Array (Nat × Nat)) : RenderCache :={ c with lineIndexMap := c.lineIndexMap.insert r idx }
let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.length
let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val |>.getD 0let lineStr := ViE.getLineFromBuffer buffer p2.row |>.getD ""let endCol := if p2.col.val < ViE.Unicode.stringWidth lineStr thenViE.Unicode.nextDisplayCol lineStr p2.col.valelsep2.col.vallet endOff := ViE.getOffsetFromPointInBuffer buffer p2.row.val endCol |>.getD buffer.table.tree.length
let start := lineStart + minCollet len := min (maxCol - minCol + 1) (if lineLen > minCol then lineLen - minCol else 0)
let start := ViE.getOffsetFromPointInBuffer buffer r minCol |>.getD (lineStart + lineLen)let endCol := maxCol + 1let endOff := ViE.getOffsetFromPointInBuffer buffer r endCol |>.getD (lineStart + lineLen)let len := if endOff > start then endOff - start else 0
let startOff := buffer.table.getOffsetFromPoint p1.row.val p1.col.val |>.getD 0let endOff := buffer.table.getOffsetFromPoint p2.row.val (p2.col.val + 1) |>.getD buffer.table.tree.length
let startOff := ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val |>.getD 0let lineStr := ViE.getLineFromBuffer buffer p2.row |>.getD ""let endCol := if p2.col.val < ViE.Unicode.stringWidth lineStr thenViE.Unicode.nextDisplayCol lineStr p2.col.valelsep2.col.vallet endOff := ViE.getOffsetFromPointInBuffer buffer p2.row.val endCol |>.getD buffer.table.tree.length
def lineString (buffer : FileBuffer) (row : Row) : String :=ViE.getLineFromBuffer buffer row |>.getD ""def lineDisplayWidth (buffer : FileBuffer) (row : Row) : Nat :=ViE.getLineLengthFromBuffer buffer row |>.getD 0def charAtDisplayCol (lineStr : String) (col : Col) : Char :=let idx := ViE.Unicode.displayColToCharIndex lineStr col.valList.getD lineStr.toList idx ' 'def nextCol (buffer : FileBuffer) (row : Row) (col : Col) : Col :=let lineStr := lineString buffer row⟨ViE.Unicode.nextDisplayCol lineStr col.val⟩
partial def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=let lineStr := ViE.getLineFromBuffer buffer row |>.getD ""let c := List.getD lineStr.toList col.val ' '
partial def findPrevStart (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=let lineStr := lineString buffer rowlet c := charAtDisplayCol lineStr col
partial def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=let lineLen := ViE.getLineLengthFromBuffer buffer row |>.getD 0
partial def findNextEnd (buffer : FileBuffer) (row : Row) (col : Col) : Row × Col :=let lineLen := lineDisplayWidth buffer row
match buffer.table.getOffsetFromPoint cursor.row.val (cursor.col.val - 1) with| some offset =>{ buffer with table := buffer.table.delete offset 1 (offset + 1)dirty := true }| none => buffer
match ViE.getOffsetFromPointInBuffer buffer cursor.row.val prevC.val,ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val with| some startOff, some endOff =>let len := endOff - startOffif len > 0 then{ buffer with table := buffer.table.delete startOff len endOffdirty := true }else buffer| _, _ => buffer
match buffer.table.getOffsetFromPoint cursor.row.val cursor.col.val with| some offset =>
match ViE.getOffsetFromPointInBuffer buffer cursor.row.val cursor.col.val,ViE.getOffsetFromPointInBuffer buffer cursor.row.val nextC.val with| some startOff, some endOff =>
match buffer.table.getLineRange cursor.row.val with| some (_, len) =>if cursor.col.val < len then{ buffer with table := buffer.table.delete offset 1 offsetdirty := true }elsebuffer| none => buffer| none => buffer
if cursor.col.val < lineLen && endOff > startOff then{ buffer with table := buffer.table.delete startOff (endOff - startOff) startOffdirty := true }elsebuffer| _, _ => buffer
match buffer.table.getOffsetFromPoint p1.row.val p1.col.val,buffer.table.getOffsetFromPoint p2.row.val p2.col.val with
match ViE.getOffsetFromPointInBuffer buffer p1.row.val p1.col.val,ViE.getOffsetFromPointInBuffer buffer p2.row.val p2.col.val with
let lineLen := ViE.getLineLengthFromBuffer buffer endP.row |>.getD 0let targetCol := if endP.col.val + 1 <= lineLen then endP.col.val + 1 else lineLen
let lineLen := lineDisplayWidth buffer endP.rowlet lineStr := lineString buffer endP.rowlet targetCol := if endP.col.val < lineLen then ViE.Unicode.nextDisplayCol lineStr endP.col.val else lineLen
-- Allow col up to len (inclusive)if col <= len then some (startOff + col)else some (startOff + len)
-- Col is a display column; convert to byte offset within the line.let lineStr := PieceTree.getSubstring pt.tree startOff len ptlet byteOff := ViE.Unicode.displayColToByteOffset lineStr collet clamped := if byteOff <= len then byteOff else lensome (startOff + clamped)
| some (r, c) => (r, c)
| some (r, c) =>match PieceTable.getLineRange pt r with| some (startOff, len) =>let rel := if c <= len then c else lenlet sub := PieceTree.getSubstring pt.tree startOff rel ptlet displayCol := ViE.Unicode.stringWidth sub(r, displayCol)| none => (r, c)
buffer.table.getLine n.val
match buffer.cache.findRaw n with| some s => some s| none => buffer.table.getLine n.val/-- Get byte offset from Row/Col (display column) using per-line index cache if available. -/def getOffsetFromPointInBuffer (buffer : FileBuffer) (row col : Nat) : Option Nat :=match buffer.table.getLineRange row with| some (startOff, len) =>let line := getLineFromBuffer buffer ⟨row⟩ |>.getD ""let byteOff := match buffer.cache.findIndex ⟨row⟩ with| some idx => ViE.Unicode.displayColToByteOffsetFromIndex idx col| none => ViE.Unicode.displayColToByteOffset line collet clamped := if byteOff <= len then byteOff else lensome (startOff + clamped)| none => none