2025-08-06 00:30:50 +01:00
|
|
|
structure SearchList =
|
2024-11-11 13:23:37 +00:00
|
|
|
struct
|
2025-08-06 00:16:50 +01:00
|
|
|
structure IntSet =
|
|
|
|
|
MakeGapSet
|
|
|
|
|
(struct
|
|
|
|
|
type key = int
|
|
|
|
|
val maxNodeSize = 32
|
2024-11-11 13:23:37 +00:00
|
|
|
|
2025-08-06 00:30:50 +01:00
|
|
|
fun l (a, b: int) = a < b
|
|
|
|
|
fun eq (a, b: int) = a = b
|
|
|
|
|
fun g (a, b: int) = a > b
|
2025-08-06 00:16:50 +01:00
|
|
|
end)
|
2024-11-11 13:23:37 +00:00
|
|
|
|
2025-08-05 13:24:55 +01:00
|
|
|
type t = IntSet.t
|
2024-11-11 13:23:37 +00:00
|
|
|
|
2025-08-05 13:24:55 +01:00
|
|
|
val empty = IntSet.empty
|
|
|
|
|
|
|
|
|
|
val goToNum = IntSet.moveTo
|
2024-11-12 07:57:36 +00:00
|
|
|
|
2025-08-06 00:30:50 +01:00
|
|
|
fun cons (num, acc) =
|
|
|
|
|
let
|
|
|
|
|
val num = Vector.fromList [num]
|
|
|
|
|
in
|
|
|
|
|
case acc of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
if Vector.length hd < 32 then (Vector.concat [num, hd]) :: tl
|
|
|
|
|
else num :: acc
|
|
|
|
|
| [] => num :: acc
|
|
|
|
|
end
|
2025-08-05 13:24:55 +01:00
|
|
|
|
2025-08-06 00:30:50 +01:00
|
|
|
fun searchStep (pos, hd, absIdx, tl, acc, searchPos, searchString) =
|
|
|
|
|
if searchPos < 0 then
|
|
|
|
|
cons (absIdx + 1, acc)
|
|
|
|
|
else if pos < 0 then
|
|
|
|
|
case tl of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
searchStep
|
|
|
|
|
(String.size hd - 1, hd, absIdx, tl, acc, searchPos, searchString)
|
|
|
|
|
| [] => 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
|
|
|
|
|
searchStep
|
|
|
|
|
(pos - 1, hd, absIdx - 1, tl, acc, searchPos - 1, searchString)
|
2025-08-05 13:24:55 +01:00
|
|
|
else
|
2025-08-06 00:30:50 +01:00
|
|
|
acc
|
|
|
|
|
end
|
2024-11-13 12:54:47 +00:00
|
|
|
|
2025-08-06 00:30:50 +01:00
|
|
|
fun loopSearch (pos, hd, absIdx, tl, acc, searchString) =
|
|
|
|
|
if pos < 0 then
|
|
|
|
|
case tl of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
loopSearch (String.size hd - 1, hd, absIdx, tl, acc, searchString)
|
|
|
|
|
| [] => acc
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val acc = searchStep
|
|
|
|
|
(pos, hd, absIdx, tl, acc, String.size searchString - 1, searchString)
|
|
|
|
|
in
|
|
|
|
|
loopSearch (pos - 1, hd, absIdx - 1, tl, acc, searchString)
|
|
|
|
|
end
|
2024-11-13 12:54:47 +00:00
|
|
|
|
2025-08-06 00:30:50 +01:00
|
|
|
(* Prerequisite: move buffer/LineGap to end *)
|
|
|
|
|
fun search (buffer: LineGap.t, searchString) =
|
2024-11-13 12:54:47 +00:00
|
|
|
let
|
2025-08-06 00:30:50 +01:00
|
|
|
val acc =
|
|
|
|
|
if String.size searchString = 0 then
|
|
|
|
|
[]
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val {leftStrings, idx = absIdx, ...} = buffer
|
|
|
|
|
in
|
|
|
|
|
case leftStrings of
|
|
|
|
|
hd :: tl =>
|
|
|
|
|
loopSearch
|
|
|
|
|
(String.size hd - 1, hd, absIdx - 1, tl, [], searchString)
|
|
|
|
|
| [] => []
|
|
|
|
|
end
|
2024-11-13 12:54:47 +00:00
|
|
|
in
|
2025-08-06 00:30:50 +01:00
|
|
|
{left = [], right = acc}
|
2024-11-13 12:54:47 +00:00
|
|
|
end
|
2024-11-24 21:38:58 +00:00
|
|
|
|
2025-08-06 00:30:50 +01:00
|
|
|
fun build (buffer, searchString) =
|
|
|
|
|
if String.size searchString > 0 then
|
|
|
|
|
let
|
|
|
|
|
val buffer = LineGap.goToEnd buffer
|
|
|
|
|
val searchList = search (buffer, searchString)
|
|
|
|
|
in
|
|
|
|
|
(buffer, searchList)
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
(buffer, empty)
|
2024-11-11 13:23:37 +00:00
|
|
|
end
|