2024-11-15 05:37:53 +00:00
|
|
|
structure BuildSearchList =
|
|
|
|
|
struct
|
|
|
|
|
fun helpNextMatch (idx, hd, tl, absIdx, searchString, matchedChrs) =
|
|
|
|
|
if idx = String.size hd then
|
|
|
|
|
case tl of
|
|
|
|
|
tlhd :: tltl =>
|
|
|
|
|
helpNextMatch (0, tlhd, tltl, absIdx, searchString, matchedChrs)
|
2024-11-24 21:38:58 +00:00
|
|
|
| [] => NONE
|
2024-11-15 05:37:53 +00:00
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val hdChr = String.sub (hd, idx)
|
|
|
|
|
val searchChr = String.sub (searchString, matchedChrs)
|
|
|
|
|
in
|
|
|
|
|
if hdChr = searchChr then
|
|
|
|
|
if matchedChrs + 1 = String.size searchString then
|
2024-11-24 21:38:58 +00:00
|
|
|
let val matchedIdx = absIdx - String.size searchString + 1
|
|
|
|
|
in SOME matchedIdx
|
2024-11-15 05:37:53 +00:00
|
|
|
end
|
|
|
|
|
else
|
2024-11-24 21:38:58 +00:00
|
|
|
helpNextMatch
|
2024-11-15 05:37:53 +00:00
|
|
|
(idx + 1, hd, tl, absIdx + 1, searchString, matchedChrs + 1)
|
|
|
|
|
else
|
|
|
|
|
helpNextMatch (idx + 1, hd, tl, absIdx + 1, searchString, 0)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun nextMatch (bufferIdx, absIdx, rightStrings, searchString) =
|
|
|
|
|
case rightStrings of
|
|
|
|
|
hd :: tl =>
|
2024-11-24 21:38:58 +00:00
|
|
|
let
|
2025-08-04 08:33:48 +01:00
|
|
|
val strIdx = Int.max (0, absIdx - bufferIdx)
|
2024-11-15 05:37:53 +00:00
|
|
|
in
|
|
|
|
|
if strIdx < String.size hd then
|
|
|
|
|
helpNextMatch (strIdx, hd, tl, absIdx, searchString, 0)
|
|
|
|
|
else
|
|
|
|
|
(case tl of
|
2024-11-24 21:38:58 +00:00
|
|
|
tlhd :: tltl =>
|
|
|
|
|
let val strIdx = strIdx - String.size hd
|
|
|
|
|
in helpNextMatch (strIdx, tlhd, tltl, absIdx, searchString, 0)
|
|
|
|
|
end
|
|
|
|
|
| [] => NONE)
|
2024-11-15 05:37:53 +00:00
|
|
|
end
|
|
|
|
|
| [] => NONE
|
|
|
|
|
|
2024-11-16 12:27:14 +00:00
|
|
|
fun helpFromStart (app, origIdx, absIdx, buffer, searchString, searchList) =
|
2024-11-15 05:37:53 +00:00
|
|
|
let
|
|
|
|
|
val buffer = LineGap.goToIdx (absIdx, buffer)
|
|
|
|
|
val {idx = bufferIdx, rightStrings, ...} = buffer
|
|
|
|
|
in
|
|
|
|
|
case nextMatch (bufferIdx, absIdx, rightStrings, searchString) of
|
|
|
|
|
SOME matchedIdx =>
|
2024-11-24 21:38:58 +00:00
|
|
|
(* Edge case: we may be searching for a string like "a"
|
|
|
|
|
* when the buffer represents "aaa aaa aaa".
|
|
|
|
|
* In this case, there will be continual matches that are consecutive
|
|
|
|
|
* and we need to check every char in the buffer which is absIdx + 1.
|
|
|
|
|
* However, we can skip to matchedIdx + 1 if matchedIdx already exists
|
|
|
|
|
* in the searchList because we know the string between
|
|
|
|
|
* [absIdx ... matchedIdx - 1] contains no matches.
|
|
|
|
|
* This check is important to preserve the set-like semaantics
|
|
|
|
|
* of the searchList too: SearchList.append does not check for this.
|
|
|
|
|
* *)
|
|
|
|
|
if SearchList.exists (matchedIdx, searchList) then
|
2024-11-16 12:27:14 +00:00
|
|
|
helpFromStart
|
2024-11-15 06:04:11 +00:00
|
|
|
(app, origIdx, matchedIdx + 1, buffer, searchString, searchList)
|
2024-11-24 21:38:58 +00:00
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val searchList = SearchList.append (matchedIdx, searchList)
|
|
|
|
|
in
|
|
|
|
|
helpFromStart
|
|
|
|
|
(app, origIdx, absIdx + 1, buffer, searchString, searchList)
|
|
|
|
|
end
|
2024-11-15 05:37:53 +00:00
|
|
|
| NONE =>
|
|
|
|
|
let
|
|
|
|
|
val buffer = LineGap.goToIdx (origIdx, buffer)
|
|
|
|
|
val searchList = SearchList.goToNum (origIdx, searchList)
|
|
|
|
|
in
|
2024-12-17 10:55:58 +00:00
|
|
|
(* todo: probably change return type to (buffer * searchList) *)
|
2024-11-15 05:40:57 +00:00
|
|
|
AppWith.searchList (app, searchList, buffer, searchString)
|
2024-11-15 05:37:53 +00:00
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
|
2024-11-16 12:27:14 +00:00
|
|
|
fun fromStart (app, cursorIdx, buffer, searchString) =
|
2024-11-15 05:37:53 +00:00
|
|
|
if String.size searchString > 0 then
|
|
|
|
|
let
|
2025-08-05 13:59:10 +01:00
|
|
|
val buffer = LineGap.goToEnd buffer
|
|
|
|
|
val searchList = SearchLineGap.search (buffer, searchString)
|
2024-11-15 05:37:53 +00:00
|
|
|
val buffer = LineGap.goToStart buffer
|
|
|
|
|
in
|
2025-08-05 13:59:10 +01:00
|
|
|
AppWith.searchList (app, searchList, buffer, searchString)
|
2024-11-15 05:37:53 +00:00
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
app
|
2024-11-16 12:27:14 +00:00
|
|
|
|
|
|
|
|
(* searches for matchedIdx within a range from the buffer instead of from start *)
|
2024-11-24 21:38:58 +00:00
|
|
|
fun helpFromRange
|
2024-11-17 09:25:01 +00:00
|
|
|
(origIdx, curIdx, finishIdx, buffer, searchString, searchList) =
|
2024-11-24 21:38:58 +00:00
|
|
|
let
|
|
|
|
|
val buffer = LineGap.goToIdx (curIdx, buffer)
|
|
|
|
|
val {idx = bufferIdx, rightStrings, ...} = buffer
|
|
|
|
|
in
|
|
|
|
|
case nextMatch (bufferIdx, curIdx, rightStrings, searchString) of
|
|
|
|
|
SOME matchedIdx =>
|
|
|
|
|
if matchedIdx > finishIdx then
|
2024-11-16 12:27:14 +00:00
|
|
|
let
|
|
|
|
|
val buffer = LineGap.goToIdx (origIdx, buffer)
|
|
|
|
|
val searchList = SearchList.goToNum (origIdx, searchList)
|
|
|
|
|
in
|
2024-11-17 09:25:01 +00:00
|
|
|
(buffer, searchList)
|
2024-11-16 12:27:14 +00:00
|
|
|
end
|
2024-11-24 21:38:58 +00:00
|
|
|
else
|
|
|
|
|
let
|
2025-03-22 05:18:25 +00:00
|
|
|
val searchList =
|
|
|
|
|
if SearchList.exists (matchedIdx, searchList) then searchList
|
|
|
|
|
else SearchList.insert (matchedIdx, searchList)
|
2024-11-24 21:38:58 +00:00
|
|
|
in
|
|
|
|
|
helpFromRange
|
|
|
|
|
( origIdx
|
|
|
|
|
, curIdx + 1
|
|
|
|
|
, finishIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, searchString
|
|
|
|
|
, searchList
|
|
|
|
|
)
|
|
|
|
|
end
|
|
|
|
|
| NONE =>
|
|
|
|
|
let
|
|
|
|
|
val buffer = LineGap.goToIdx (origIdx, buffer)
|
|
|
|
|
val searchList = SearchList.goToNum (origIdx, searchList)
|
|
|
|
|
in
|
|
|
|
|
(buffer, searchList)
|
|
|
|
|
end
|
|
|
|
|
end
|
2024-11-16 12:27:14 +00:00
|
|
|
|
2024-11-17 09:25:01 +00:00
|
|
|
fun fromRange (startIdx, length, buffer, searchString, searchList) =
|
2025-08-05 13:59:10 +01:00
|
|
|
let
|
|
|
|
|
val buffer = LineGap.goToEnd buffer
|
|
|
|
|
val searchList = SearchLineGap.search (buffer, searchString)
|
|
|
|
|
val buffer = LineGap.goToStart buffer
|
|
|
|
|
in
|
2025-08-04 09:03:47 +01:00
|
|
|
(buffer, searchList)
|
2025-08-05 13:59:10 +01:00
|
|
|
end
|
2024-11-15 05:37:53 +00:00
|
|
|
end
|