only update search list if timestamp for search message is greater than the buffer's modified time
This commit is contained in:
@@ -49,14 +49,21 @@ struct
|
||||
)
|
||||
end
|
||||
|
||||
fun withSearchList (app: app_type, searchList) =
|
||||
fun withSearchList (app: app_type, searchList, searchTime) =
|
||||
let
|
||||
val {buffer, searchString, cursorIdx, bufferModifyTime, ...} = app
|
||||
val app = NormalModeWith.searchList
|
||||
(app, searchList, buffer, searchString, bufferModifyTime)
|
||||
open Time
|
||||
in
|
||||
buildTextAndClear
|
||||
(app, buffer, cursorIdx, searchList, [], bufferModifyTime)
|
||||
if searchTime >= #bufferModifyTime app then
|
||||
let
|
||||
val {buffer, searchString, cursorIdx, bufferModifyTime, ...} = app
|
||||
val app = NormalModeWith.searchList
|
||||
(app, searchList, buffer, searchString, bufferModifyTime)
|
||||
in
|
||||
buildTextAndClear
|
||||
(app, buffer, cursorIdx, searchList, [], bufferModifyTime)
|
||||
end
|
||||
else
|
||||
app
|
||||
end
|
||||
|
||||
fun resizeText (app: app_type, newWidth, newHeight) =
|
||||
|
||||
Reference in New Issue
Block a user