2025-08-06 00:30:50 +01:00
|
|
|
structure SearchList =
|
2024-11-11 13:23:37 +00:00
|
|
|
struct
|
2025-08-06 00:42:24 +01:00
|
|
|
type t = int vector
|
2024-11-11 13:23:37 +00:00
|
|
|
|
2025-08-06 00:42:24 +01:00
|
|
|
val empty = Vector.fromList []
|
2025-08-05 13:24:55 +01:00
|
|
|
|
2025-08-30 23:05:11 +01:00
|
|
|
fun loopSearch (pos, hd, absIdx, tl, acc, searchPos, searchString) =
|
|
|
|
|
if pos = String.size hd then
|
2025-08-06 00:30:50 +01:00
|
|
|
case tl of
|
2025-08-30 23:05:11 +01:00
|
|
|
hd :: tl => loopSearch (0, hd, absIdx, tl, acc, searchPos, searchString)
|
2025-08-06 00:30:50 +01:00
|
|
|
| [] => acc
|
2024-11-16 09:05:47 +00:00
|
|
|
else
|
2025-08-06 00:30:50 +01:00
|
|
|
let
|
|
|
|
|
val bufferChr = String.sub (hd, pos)
|
|
|
|
|
val searchChr = String.sub (searchString, searchPos)
|
|
|
|
|
in
|
|
|
|
|
if bufferChr = searchChr then
|
2025-08-30 23:05:11 +01:00
|
|
|
if searchPos + 1 = String.size searchString then
|
|
|
|
|
(* we fully matched the search string *)
|
|
|
|
|
let
|
|
|
|
|
val foundIdx = absIdx - String.size searchString + 1
|
|
|
|
|
val acc = PersistentVector.append (foundIdx, acc)
|
|
|
|
|
in
|
|
|
|
|
loopSearch (pos + 1, hd, absIdx + 1, tl, acc, 0, searchString)
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
loopSearch
|
|
|
|
|
(pos + 1, hd, absIdx + 1, tl, acc, searchPos + 1, searchString)
|
|
|
|
|
else if searchPos = 0 then
|
|
|
|
|
loopSearch (pos + 1, hd, absIdx + 1, tl, acc, 0, searchString)
|
2025-08-05 13:24:55 +01:00
|
|
|
else
|
2025-08-30 23:05:11 +01:00
|
|
|
loopSearch (pos, hd, absIdx, tl, acc, 0, searchString)
|
2025-08-06 00:30:50 +01:00
|
|
|
end
|
2024-11-13 12:54:47 +00:00
|
|
|
|
2025-08-30 23:05:11 +01:00
|
|
|
fun search ({rightStrings, leftStrings, ...}: LineGap.t, searchString) =
|
|
|
|
|
case rightStrings of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
let
|
|
|
|
|
val result = loopSearch
|
|
|
|
|
(0, hd, 0, tl, PersistentVector.empty, 0, searchString)
|
|
|
|
|
in
|
|
|
|
|
PersistentVector.toVector result
|
|
|
|
|
end
|
|
|
|
|
| [] => empty
|
2024-11-24 21:38:58 +00:00
|
|
|
|
2025-08-07 15:28:29 +01:00
|
|
|
(* Prerequisite: move buffer/LineGap to end *)
|
2025-08-06 00:30:50 +01:00
|
|
|
fun build (buffer, searchString) =
|
2025-08-07 15:28:29 +01:00
|
|
|
if String.size searchString > 0 then search (buffer, searchString)
|
|
|
|
|
else empty
|
2025-08-07 13:12:04 +01:00
|
|
|
|
|
|
|
|
fun loopNextMatch (pos, searchList, count) =
|
|
|
|
|
if count = 0 then
|
|
|
|
|
Vector.sub (searchList, pos)
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val pos = pos + 1
|
|
|
|
|
val pos = if pos < Vector.length searchList then pos else 0
|
|
|
|
|
val count = count - 1
|
|
|
|
|
in
|
|
|
|
|
loopNextMatch (pos, searchList, count)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun nextMatch (cursorIdx, searchList, count) =
|
|
|
|
|
if Vector.length searchList = 0 then
|
|
|
|
|
~1
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val pos = BinSearch.equalOrMore (cursorIdx + 1, searchList)
|
|
|
|
|
val pos = if pos < Vector.length searchList then pos else 0
|
|
|
|
|
val count = count - 1
|
|
|
|
|
in
|
|
|
|
|
loopNextMatch (pos, searchList, count)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun loopPrevMatch (pos, searchList, count) =
|
|
|
|
|
if count = 0 then
|
|
|
|
|
Vector.sub (searchList, pos)
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val pos = pos - 1
|
|
|
|
|
val pos = if pos < 0 then Vector.length searchList - 1 else pos
|
|
|
|
|
val count = count - 1
|
|
|
|
|
in
|
|
|
|
|
loopPrevMatch (pos, searchList, count)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun prevMatch (cursorIdx, searchList, count) =
|
|
|
|
|
if Vector.length searchList = 0 then
|
|
|
|
|
~1
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val pos = BinSearch.equalOrLess (cursorIdx - 1, searchList)
|
|
|
|
|
val pos = if pos < 0 then Vector.length searchList - 1 else pos
|
|
|
|
|
val count = count - 1
|
|
|
|
|
in
|
|
|
|
|
loopPrevMatch (pos, searchList, count)
|
|
|
|
|
end
|
2025-08-07 15:28:29 +01:00
|
|
|
|
|
|
|
|
fun rangeSearchStep (pos, hd, absIdx, tl, acc, searchPos, searchString, low) =
|
|
|
|
|
if searchPos < 0 then
|
2025-08-30 18:12:47 +01:00
|
|
|
raise Fail "todo"
|
2025-08-07 15:28:29 +01:00
|
|
|
else if absIdx < low then
|
|
|
|
|
acc
|
|
|
|
|
else if pos < 0 then
|
|
|
|
|
case tl of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
rangeSearchStep
|
|
|
|
|
( String.size hd - 1
|
|
|
|
|
, hd
|
|
|
|
|
, absIdx
|
|
|
|
|
, tl
|
|
|
|
|
, acc
|
|
|
|
|
, searchPos
|
|
|
|
|
, searchString
|
|
|
|
|
, low
|
|
|
|
|
)
|
|
|
|
|
| [] => acc
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val bufferChr = String.sub (hd, pos)
|
|
|
|
|
val searchChr = String.sub (searchString, searchPos)
|
|
|
|
|
in
|
|
|
|
|
if bufferChr = searchChr then
|
|
|
|
|
rangeSearchStep
|
|
|
|
|
(pos - 1, hd, absIdx - 1, tl, acc, searchPos - 1, searchString, low)
|
|
|
|
|
else
|
|
|
|
|
acc
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun loopRange (pos, hd, absIdx, tl, acc, searchString, low) =
|
|
|
|
|
if absIdx < low then
|
|
|
|
|
Vector.fromList acc
|
|
|
|
|
else if pos < 0 then
|
|
|
|
|
case tl of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
loopRange (String.size hd - 1, hd, absIdx, tl, acc, searchString, low)
|
|
|
|
|
| [] => Vector.fromList acc
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val acc = rangeSearchStep
|
|
|
|
|
( pos
|
|
|
|
|
, hd
|
|
|
|
|
, absIdx
|
|
|
|
|
, tl
|
|
|
|
|
, acc
|
|
|
|
|
, String.size searchString - 1
|
|
|
|
|
, searchString
|
|
|
|
|
, low
|
|
|
|
|
)
|
|
|
|
|
in
|
|
|
|
|
loopRange (pos - 1, hd, absIdx - 1, tl, acc, searchString, low)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun searchRange (buffer: LineGap.t, searchString, low) =
|
|
|
|
|
let
|
2025-08-07 15:37:32 +01:00
|
|
|
val low = Int.max (low, 0)
|
2025-08-07 15:28:29 +01:00
|
|
|
val {rightStrings, leftStrings, idx = absIdx, ...} = buffer
|
|
|
|
|
in
|
|
|
|
|
case rightStrings of
|
|
|
|
|
hd :: _ =>
|
|
|
|
|
let
|
|
|
|
|
val pos = String.size hd - 1
|
|
|
|
|
val absIdx = absIdx + String.size hd - 1
|
|
|
|
|
in
|
|
|
|
|
loopRange (pos, hd, absIdx, leftStrings, [], searchString, low)
|
|
|
|
|
end
|
|
|
|
|
| [] =>
|
|
|
|
|
(case leftStrings of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
let
|
|
|
|
|
val pos = String.size hd - 1
|
|
|
|
|
val absIdx = absIdx - 1
|
|
|
|
|
in
|
|
|
|
|
loopRange (pos, hd, absIdx, tl, [], searchString, low)
|
|
|
|
|
end
|
|
|
|
|
| [] => empty)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun buildRange (buffer, searchString, low) =
|
|
|
|
|
if String.size searchString > 0 then searchRange (buffer, searchString, low)
|
|
|
|
|
else empty
|
2024-11-11 13:23:37 +00:00
|
|
|
end
|