2025-09-01 03:04:39 +01:00
|
|
|
structure NormalSearchFinish =
|
|
|
|
|
struct
|
|
|
|
|
open AppType
|
2025-09-01 12:52:26 +01:00
|
|
|
open DrawMsg
|
2025-09-01 03:04:39 +01:00
|
|
|
|
2025-09-01 03:18:45 +01:00
|
|
|
fun onSearchChanged
|
2025-09-14 09:50:07 +01:00
|
|
|
( app: app_type
|
|
|
|
|
, searchString
|
|
|
|
|
, tempSearchList
|
|
|
|
|
, searchCursorIdx
|
|
|
|
|
, searchScrollColumn
|
|
|
|
|
, buffer
|
|
|
|
|
) =
|
2025-09-01 03:04:39 +01:00
|
|
|
let
|
2025-09-12 13:02:32 +01:00
|
|
|
val
|
|
|
|
|
{ buffer
|
|
|
|
|
, cursorIdx
|
2025-09-13 05:12:17 +01:00
|
|
|
, startLine = prevLineNumber
|
2025-09-12 13:02:32 +01:00
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, visualScrollColumn
|
|
|
|
|
, ...
|
|
|
|
|
} = app
|
2025-09-13 05:12:17 +01:00
|
|
|
|
2025-09-14 09:50:07 +01:00
|
|
|
val searchScrollColumn =
|
|
|
|
|
TextScroll.getScrollColumnFromString
|
|
|
|
|
(searchCursorIdx, windowWidth, searchScrollColumn)
|
|
|
|
|
|
2025-09-01 03:18:45 +01:00
|
|
|
val mode = NORMAL_SEARCH_MODE
|
|
|
|
|
{ searchString = searchString
|
|
|
|
|
, tempSearchList = tempSearchList
|
|
|
|
|
, searchCursorIdx = searchCursorIdx
|
2025-09-14 09:50:07 +01:00
|
|
|
, searchScrollColumn = searchScrollColumn
|
2025-09-01 03:18:45 +01:00
|
|
|
}
|
2025-09-01 03:04:39 +01:00
|
|
|
|
|
|
|
|
val floatWindowWidth = Real32.fromInt windowWidth
|
|
|
|
|
val floatWindowHeight = Real32.fromInt windowHeight
|
|
|
|
|
|
|
|
|
|
val searchStringPosY = windowHeight - TextConstants.ySpace - 5
|
|
|
|
|
|
2025-09-14 09:14:22 +01:00
|
|
|
val initialTextAcc = SearchBar.build
|
2025-09-01 03:04:39 +01:00
|
|
|
( searchString
|
|
|
|
|
, 5
|
|
|
|
|
, searchStringPosY
|
|
|
|
|
, windowWidth
|
|
|
|
|
, floatWindowWidth
|
|
|
|
|
, floatWindowHeight
|
2025-09-14 09:14:22 +01:00
|
|
|
, searchCursorIdx
|
2025-09-14 10:07:43 +01:00
|
|
|
, searchScrollColumn
|
2025-09-01 03:04:39 +01:00
|
|
|
)
|
|
|
|
|
|
2025-09-13 05:12:17 +01:00
|
|
|
val buffer = LineGap.goToIdx (cursorIdx, buffer)
|
2025-09-16 22:20:55 +01:00
|
|
|
val cursorLine = LineGap.idxToLineNumber (cursorIdx, buffer)
|
2025-09-13 05:12:17 +01:00
|
|
|
val startLine =
|
2025-09-19 23:17:28 +01:00
|
|
|
TextScroll.getStartLine
|
|
|
|
|
(prevLineNumber, cursorLine, windowHeight, #lineLength buffer)
|
2025-09-01 03:04:39 +01:00
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
|
|
|
|
|
val remainingWindowHeight = windowHeight - (TextConstants.ySpace * 2)
|
|
|
|
|
|
2025-09-12 13:02:32 +01:00
|
|
|
val drawMsg = NormalModeTextBuilder.startBuild
|
2025-09-01 03:04:39 +01:00
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, remainingWindowHeight
|
|
|
|
|
, floatWindowWidth
|
|
|
|
|
, floatWindowHeight
|
|
|
|
|
, tempSearchList
|
2025-09-12 13:02:32 +01:00
|
|
|
, visualScrollColumn
|
2025-09-14 09:14:22 +01:00
|
|
|
, initialTextAcc
|
2025-09-01 03:04:39 +01:00
|
|
|
)
|
2025-09-12 13:02:32 +01:00
|
|
|
val drawMsg = Vector.concat drawMsg
|
2025-09-12 14:02:38 +01:00
|
|
|
val drawMsg = DrawMsg.DRAW_TEXT drawMsg
|
|
|
|
|
val msgs = [MailboxType.DRAW drawMsg]
|
2025-09-01 03:04:39 +01:00
|
|
|
in
|
|
|
|
|
NormalSearchModeWith.changeTempSearchString
|
|
|
|
|
(app, buffer, startLine, mode, msgs)
|
|
|
|
|
end
|
|
|
|
|
|
2025-09-01 12:52:26 +01:00
|
|
|
fun resize
|
|
|
|
|
( app: app_type
|
|
|
|
|
, newWindowWidth
|
|
|
|
|
, newWindowHeight
|
2025-09-14 10:28:42 +01:00
|
|
|
, searchString
|
2025-09-01 12:52:26 +01:00
|
|
|
, searchCursorIdx
|
|
|
|
|
, tempSearchList
|
2025-09-14 10:07:43 +01:00
|
|
|
, searchScrollColumn
|
2025-09-01 12:52:26 +01:00
|
|
|
) =
|
|
|
|
|
let
|
2025-09-13 05:12:17 +01:00
|
|
|
val
|
2025-09-14 10:28:42 +01:00
|
|
|
{buffer, cursorIdx, startLine = prevLineNumber, visualScrollColumn, ...} =
|
|
|
|
|
app
|
2025-09-01 12:52:26 +01:00
|
|
|
|
|
|
|
|
val floatWindowWidth = Real32.fromInt newWindowWidth
|
|
|
|
|
val floatWindowHeight = Real32.fromInt newWindowHeight
|
|
|
|
|
|
2025-09-14 10:28:42 +01:00
|
|
|
val searchScrollColumn =
|
|
|
|
|
TextScroll.getScrollColumnFromString
|
|
|
|
|
(searchCursorIdx, newWindowWidth, searchScrollColumn)
|
|
|
|
|
|
|
|
|
|
val mode = NORMAL_SEARCH_MODE
|
|
|
|
|
{ searchString = searchString
|
|
|
|
|
, tempSearchList = tempSearchList
|
|
|
|
|
, searchCursorIdx = searchCursorIdx
|
|
|
|
|
, searchScrollColumn = searchScrollColumn
|
|
|
|
|
}
|
|
|
|
|
|
2025-09-01 12:52:26 +01:00
|
|
|
val searchStringPosY = newWindowHeight - TextConstants.ySpace - 5
|
|
|
|
|
|
2025-09-14 09:14:22 +01:00
|
|
|
val initialTextAcc = SearchBar.build
|
2025-09-01 12:52:26 +01:00
|
|
|
( searchString
|
|
|
|
|
, 5
|
|
|
|
|
, searchStringPosY
|
|
|
|
|
, newWindowWidth
|
|
|
|
|
, floatWindowWidth
|
|
|
|
|
, floatWindowHeight
|
2025-09-14 09:14:22 +01:00
|
|
|
, searchCursorIdx
|
2025-09-14 10:07:43 +01:00
|
|
|
, searchScrollColumn
|
2025-09-01 12:52:26 +01:00
|
|
|
)
|
|
|
|
|
|
2025-09-13 05:12:17 +01:00
|
|
|
val buffer = LineGap.goToIdx (cursorIdx, buffer)
|
2025-09-16 22:20:55 +01:00
|
|
|
val cursorLine = LineGap.idxToLineNumber (cursorIdx, buffer)
|
2025-09-13 05:12:17 +01:00
|
|
|
val startLine =
|
2025-09-19 23:17:28 +01:00
|
|
|
TextScroll.getStartLine
|
|
|
|
|
(prevLineNumber, cursorLine, newWindowHeight, #lineLength buffer)
|
2025-09-01 12:52:26 +01:00
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
|
|
|
|
|
val remainingWindowHeight = newWindowHeight - (TextConstants.ySpace * 2)
|
|
|
|
|
|
2025-09-12 13:02:32 +01:00
|
|
|
val drawMsg = NormalModeTextBuilder.startBuild
|
2025-09-01 12:52:26 +01:00
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, newWindowWidth
|
|
|
|
|
, remainingWindowHeight
|
|
|
|
|
, floatWindowWidth
|
|
|
|
|
, floatWindowHeight
|
|
|
|
|
, tempSearchList
|
2025-09-12 13:02:32 +01:00
|
|
|
, visualScrollColumn
|
2025-09-14 10:28:42 +01:00
|
|
|
, initialTextAcc
|
2025-09-01 12:52:26 +01:00
|
|
|
)
|
2025-09-12 13:02:32 +01:00
|
|
|
val drawMsg = Vector.concat drawMsg
|
2025-09-12 14:02:38 +01:00
|
|
|
val drawMsg = DrawMsg.DRAW_TEXT drawMsg
|
|
|
|
|
val msgs = [MailboxType.DRAW drawMsg]
|
2025-09-01 12:52:26 +01:00
|
|
|
in
|
|
|
|
|
NormalSearchModeWith.bufferAndSize
|
2025-09-14 10:28:42 +01:00
|
|
|
(app, mode, buffer, newWindowWidth, newWindowHeight, msgs)
|
2025-09-01 12:52:26 +01:00
|
|
|
end
|
2025-09-01 03:04:39 +01:00
|
|
|
end
|