handle edge case in line_gap.sml when deleting to the left: we sometimes need to delete to the end of the string, so add a branch handling that case
This commit is contained in:
@@ -1971,6 +1971,55 @@ struct
|
|||||||
)
|
)
|
||||||
end
|
end
|
||||||
else if prevIdx < start then
|
else if prevIdx < start then
|
||||||
|
if finish >= curIdx then
|
||||||
|
(* delete from end of string *)
|
||||||
|
let
|
||||||
|
val oldNodeTextLength = String.size leftStringsHd
|
||||||
|
val oldNodeLineLength = Vector.length leftLinesHd
|
||||||
|
|
||||||
|
val sub1Length = start - prevIdx
|
||||||
|
val sub1 = String.substring (leftStringsHd, 0, sub1Length)
|
||||||
|
val sub1Lines =
|
||||||
|
if Vector.length leftLinesHd > 0 then
|
||||||
|
let
|
||||||
|
val midpoint = binSearch
|
||||||
|
(String.size sub1 - 1, leftLinesHd)
|
||||||
|
in
|
||||||
|
if midpoint >= 0 then
|
||||||
|
let
|
||||||
|
val slice = VectorSlice.slice
|
||||||
|
(leftLinesHd, 0, SOME (midpoint + 1))
|
||||||
|
in
|
||||||
|
VectorSlice.vector slice
|
||||||
|
end
|
||||||
|
else
|
||||||
|
Vector.fromList []
|
||||||
|
end
|
||||||
|
else
|
||||||
|
leftLinesHd
|
||||||
|
val newNodeTextLength = String.size sub1
|
||||||
|
val textLengthDifference =
|
||||||
|
oldNodeTextLength - newNodeTextLength
|
||||||
|
val textLength = textLength - textLengthDifference
|
||||||
|
|
||||||
|
val newNodeLineLength = Vector.length sub1Lines
|
||||||
|
val lineLengthDifference =
|
||||||
|
oldNodeLineLength - newNodeLineLength
|
||||||
|
val lineLength = lineLength - lineLengthDifference
|
||||||
|
in
|
||||||
|
{ idx = prevIdx + String.size sub1
|
||||||
|
, line =
|
||||||
|
(curLine - Vector.length leftLinesHd)
|
||||||
|
+ Vector.length sub1Lines
|
||||||
|
, leftStrings = sub1 :: leftStringsTl
|
||||||
|
, leftLines = sub1Lines :: leftLinesTl
|
||||||
|
, rightStrings = rightStrings
|
||||||
|
, rightLines = rightLines
|
||||||
|
, textLength = textLength
|
||||||
|
, lineLength = lineLength
|
||||||
|
}
|
||||||
|
end
|
||||||
|
else
|
||||||
(* We want to delete in the middle of leftStringsHd.
|
(* We want to delete in the middle of leftStringsHd.
|
||||||
* We also have to delete in the middle of leftLinesHd in order to
|
* We also have to delete in the middle of leftLinesHd in order to
|
||||||
* do this. *)
|
* do this. *)
|
||||||
|
|||||||
Reference in New Issue
Block a user