2025-08-31 06:28:05 +01:00
|
|
|
structure NormalFinish =
|
2025-01-09 22:30:51 +00:00
|
|
|
struct
|
|
|
|
|
open AppType
|
|
|
|
|
|
2025-08-07 17:41:10 +01:00
|
|
|
open MailboxType
|
|
|
|
|
open DrawMsg
|
|
|
|
|
open InputMsg
|
|
|
|
|
|
|
|
|
|
fun clearMode app =
|
2025-08-31 06:28:05 +01:00
|
|
|
NormalModeWith.mode (app, NORMAL_MODE "", [])
|
2025-08-07 17:41:10 +01:00
|
|
|
|
2025-08-20 12:51:31 +01:00
|
|
|
fun buildTextAndClear
|
|
|
|
|
(app: app_type, buffer, cursorIdx, searchList, msgs, bufferModifyTime) =
|
2025-01-09 22:30:51 +00:00
|
|
|
let
|
2025-09-13 05:12:17 +01:00
|
|
|
val
|
|
|
|
|
{ windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, searchString
|
|
|
|
|
, visualScrollColumn = prevScrollColumn
|
|
|
|
|
, startLine = prevLineNumber
|
|
|
|
|
, ...
|
|
|
|
|
} = app
|
2025-01-09 22:30:51 +00:00
|
|
|
|
2025-09-13 05:12:17 +01:00
|
|
|
(* calculate new scroll column and start line, if there are any changes *)
|
2025-09-11 16:17:56 +01:00
|
|
|
val buffer = LineGap.goToIdx (cursorIdx, buffer)
|
2025-09-11 23:43:09 +01:00
|
|
|
val visualScrollColumn =
|
2025-09-13 05:12:17 +01:00
|
|
|
TextScroll.getScrollColumn
|
|
|
|
|
(buffer, cursorIdx, windowWidth, prevScrollColumn)
|
2025-01-09 22:30:51 +00:00
|
|
|
|
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-01-09 22:30:51 +00:00
|
|
|
|
|
|
|
|
(* move buffer to new startLine as required by TextBuilder.build *)
|
|
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
|
2025-09-12 12:49:19 +01:00
|
|
|
val drawMsg = NormalModeTextBuilder.build
|
2025-01-09 22:30:51 +00:00
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, searchList
|
2025-09-12 12:49:19 +01:00
|
|
|
, visualScrollColumn
|
2025-01-09 22:30:51 +00:00
|
|
|
)
|
2025-09-12 12:49:19 +01:00
|
|
|
val drawMsg = Vector.concat drawMsg
|
2025-09-12 13:47:14 +01:00
|
|
|
val drawMsg = DRAW_TEXT drawMsg
|
2025-09-12 23:21:53 +01:00
|
|
|
val msgs = DRAW drawMsg :: msgs
|
2025-01-09 22:30:51 +00:00
|
|
|
|
|
|
|
|
val mode = NORMAL_MODE ""
|
|
|
|
|
in
|
2025-08-31 06:28:05 +01:00
|
|
|
NormalModeWith.bufferAndCursorIdx
|
2025-08-20 12:51:31 +01:00
|
|
|
( app
|
|
|
|
|
, buffer
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, mode
|
|
|
|
|
, startLine
|
|
|
|
|
, searchList
|
|
|
|
|
, msgs
|
|
|
|
|
, bufferModifyTime
|
2025-09-11 23:43:09 +01:00
|
|
|
, visualScrollColumn
|
2025-08-20 12:51:31 +01:00
|
|
|
)
|
2025-01-09 22:30:51 +00:00
|
|
|
end
|
2025-08-07 17:41:10 +01:00
|
|
|
|
2025-09-07 13:37:14 +01:00
|
|
|
fun withSearchList (app: app_type, searchList, searchTime) =
|
2025-08-07 17:41:10 +01:00
|
|
|
let
|
2025-09-07 13:37:14 +01:00
|
|
|
open Time
|
2025-08-07 17:41:10 +01:00
|
|
|
in
|
2025-09-07 13:37:14 +01:00
|
|
|
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
|
2025-08-07 17:41:10 +01:00
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun resizeText (app: app_type, newWidth, newHeight) =
|
|
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, searchList
|
|
|
|
|
, searchString
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime
|
2025-09-13 01:43:31 +01:00
|
|
|
, visualScrollColumn = prevScrollColumn
|
2025-08-07 17:41:10 +01:00
|
|
|
, ...
|
|
|
|
|
} = app
|
|
|
|
|
|
2025-09-11 23:43:09 +01:00
|
|
|
val newBuffer = LineGap.goToIdx (cursorIdx, buffer)
|
|
|
|
|
val visualScrollColumn =
|
2025-09-13 05:12:17 +01:00
|
|
|
TextScroll.getScrollColumn
|
2025-09-13 05:31:11 +01:00
|
|
|
(newBuffer, cursorIdx, newWidth, prevScrollColumn)
|
2025-09-11 23:43:09 +01:00
|
|
|
val newBuffer = LineGap.goToLine (startLine, newBuffer)
|
2025-09-12 12:49:19 +01:00
|
|
|
val lineIdx = TextBuilderUtils.getLineAbsIdxFromBuffer (startLine, buffer)
|
2025-08-07 17:41:10 +01:00
|
|
|
|
2025-09-12 12:49:19 +01:00
|
|
|
val drawMsg = NormalModeTextBuilder.build
|
2025-08-07 17:41:10 +01:00
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
2025-09-12 12:49:19 +01:00
|
|
|
, buffer
|
2025-09-12 23:21:53 +01:00
|
|
|
, newWidth
|
|
|
|
|
, newHeight
|
2025-08-07 17:41:10 +01:00
|
|
|
, searchList
|
2025-09-12 12:49:19 +01:00
|
|
|
, visualScrollColumn
|
2025-08-07 17:41:10 +01:00
|
|
|
)
|
2025-09-12 12:49:19 +01:00
|
|
|
val drawMsg = Vector.concat drawMsg
|
2025-09-12 13:47:14 +01:00
|
|
|
val drawMsg = DRAW_TEXT drawMsg
|
2025-09-12 23:21:53 +01:00
|
|
|
val msgs = [DRAW drawMsg]
|
2025-08-07 17:41:10 +01:00
|
|
|
in
|
2025-08-31 06:28:05 +01:00
|
|
|
NormalModeWith.bufferAndSize
|
2025-08-20 12:51:31 +01:00
|
|
|
( app
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newWidth
|
|
|
|
|
, newHeight
|
|
|
|
|
, searchList
|
2025-09-12 23:21:53 +01:00
|
|
|
, msgs
|
2025-08-20 12:51:31 +01:00
|
|
|
, bufferModifyTime
|
2025-09-11 23:43:09 +01:00
|
|
|
, visualScrollColumn
|
2025-08-20 12:51:31 +01:00
|
|
|
)
|
2025-08-07 17:41:10 +01:00
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun centreToCursor (app: app_type) =
|
|
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
2025-09-13 05:12:17 +01:00
|
|
|
, startLine = prevLineNumber
|
2025-08-07 17:41:10 +01:00
|
|
|
, cursorIdx
|
|
|
|
|
, searchList
|
|
|
|
|
, searchString
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime
|
2025-09-12 12:49:19 +01:00
|
|
|
, visualScrollColumn
|
2025-08-07 17:41:10 +01:00
|
|
|
, ...
|
|
|
|
|
} = app
|
|
|
|
|
|
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 18:23:55 +01:00
|
|
|
val startLine = TextScroll.getLineCentre (cursorLine, windowHeight)
|
2025-08-07 17:41:10 +01:00
|
|
|
|
|
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
2025-09-12 12:49:19 +01:00
|
|
|
val drawMsg = NormalModeTextBuilder.build
|
2025-08-07 17:41:10 +01:00
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, searchList
|
2025-09-12 12:49:19 +01:00
|
|
|
, visualScrollColumn
|
2025-08-07 17:41:10 +01:00
|
|
|
)
|
2025-09-12 12:49:19 +01:00
|
|
|
val drawMsg = Vector.concat drawMsg
|
2025-09-12 13:47:14 +01:00
|
|
|
val drawMsg = DRAW_TEXT drawMsg
|
|
|
|
|
val drawMsg = [DRAW drawMsg]
|
2025-08-07 17:41:10 +01:00
|
|
|
in
|
2025-09-13 05:12:17 +01:00
|
|
|
NormalModeWith.bufferAndCursorIdx
|
|
|
|
|
( app
|
|
|
|
|
, buffer
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, NORMAL_MODE ""
|
|
|
|
|
, startLine
|
|
|
|
|
, searchList
|
|
|
|
|
, drawMsg
|
|
|
|
|
, bufferModifyTime
|
|
|
|
|
, #visualScrollColumn app
|
|
|
|
|
)
|
2025-08-07 17:41:10 +01:00
|
|
|
end
|
2025-01-09 22:30:51 +00:00
|
|
|
end
|