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
|
|
|
|
|
val {windowWidth, windowHeight, startLine, searchString, ...} = app
|
|
|
|
|
|
2025-09-11 16:17:56 +01:00
|
|
|
(* calculate scroll column *)
|
|
|
|
|
val buffer = LineGap.goToIdx (cursorIdx, buffer)
|
2025-09-11 23:43:09 +01:00
|
|
|
val visualScrollColumn =
|
|
|
|
|
TextScroll.getScrollColumn (buffer, cursorIdx, windowWidth)
|
2025-09-11 16:17:56 +01:00
|
|
|
|
2025-08-07 13:37:03 +01:00
|
|
|
(* move LineGap to first line displayed on screen *)
|
2025-01-09 22:30:51 +00:00
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
|
|
|
|
|
(* get new startLine which may move screen depending on cursor movements *)
|
|
|
|
|
val startLine = TextWindow.getStartLine
|
|
|
|
|
(buffer, startLine, cursorIdx, windowWidth, windowHeight)
|
|
|
|
|
|
|
|
|
|
(* move buffer to new startLine as required by TextBuilder.build *)
|
|
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
|
2025-08-07 12:20:57 +01:00
|
|
|
val msgs = TextBuilder.build
|
2025-01-09 22:30:51 +00:00
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, searchList
|
|
|
|
|
, searchString
|
2025-08-07 12:20:57 +01:00
|
|
|
, 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-08-07 17:41:10 +01:00
|
|
|
, ...
|
|
|
|
|
} = app
|
|
|
|
|
|
2025-09-11 23:43:09 +01:00
|
|
|
val newBuffer = LineGap.goToIdx (cursorIdx, buffer)
|
|
|
|
|
val visualScrollColumn =
|
|
|
|
|
TextScroll.getScrollColumn (buffer, cursorIdx, windowWidth)
|
|
|
|
|
val newBuffer = LineGap.goToLine (startLine, newBuffer)
|
2025-08-07 17:41:10 +01:00
|
|
|
val lineIdx = TextBuilder.getLineAbsIdx (startLine, buffer)
|
|
|
|
|
|
|
|
|
|
val drawMsg = TextBuilder.build
|
|
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newWidth
|
|
|
|
|
, newHeight
|
|
|
|
|
, searchList
|
|
|
|
|
, searchString
|
|
|
|
|
, []
|
|
|
|
|
)
|
|
|
|
|
in
|
2025-08-31 06:28:05 +01:00
|
|
|
NormalModeWith.bufferAndSize
|
2025-08-20 12:51:31 +01:00
|
|
|
( app
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newWidth
|
|
|
|
|
, newHeight
|
|
|
|
|
, searchList
|
|
|
|
|
, drawMsg
|
|
|
|
|
, 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
|
|
|
|
|
|
|
|
|
|
(* Difference between this and buildTextAndClear is that
|
|
|
|
|
* this is meant to be called after a chr movement,
|
|
|
|
|
* where the cursor may possibly jump off window by a wide marigin.
|
|
|
|
|
* Since the cursor may move away a lot, it is best to recenter.
|
|
|
|
|
* *)
|
|
|
|
|
fun buildTextAndClearAfterChr
|
2025-08-20 12:50:39 +01:00
|
|
|
(app: app_type, buffer, cursorIdx, searchList, initialMsg, bufferModifyTime) =
|
2025-08-07 17:41:10 +01:00
|
|
|
let
|
|
|
|
|
val {windowWidth, windowHeight, startLine, searchString, ...} = app
|
|
|
|
|
|
2025-09-11 23:43:09 +01:00
|
|
|
val buffer = LineGap.goToIdx (cursorIdx, buffer)
|
|
|
|
|
val visualScrollColumn =
|
|
|
|
|
TextScroll.getScrollColumn (buffer, cursorIdx, windowWidth)
|
|
|
|
|
|
2025-08-07 17:41:10 +01:00
|
|
|
(* move LineGap to first line displayed on screen *)
|
|
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
|
|
|
|
|
(* get new startLine which may move screen depending on cursor movements *)
|
|
|
|
|
val startLine = TextWindow.getStartLine
|
|
|
|
|
(buffer, startLine, cursorIdx, windowWidth, windowHeight)
|
|
|
|
|
|
|
|
|
|
(* move buffer to new startLine as required by TextBuilder.build
|
|
|
|
|
* and move searchList to idx where line starts as well *)
|
|
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
|
|
|
|
|
val drawMsg = TextBuilder.build
|
|
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, searchList
|
|
|
|
|
, searchString
|
|
|
|
|
, []
|
|
|
|
|
)
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
, drawMsg
|
|
|
|
|
, 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
|
|
|
|
|
, startLine = origLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, searchList
|
|
|
|
|
, searchString
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime
|
2025-08-07 17:41:10 +01:00
|
|
|
, ...
|
|
|
|
|
} = app
|
|
|
|
|
val buffer = LineGap.goToIdx (cursorIdx, buffer)
|
|
|
|
|
|
|
|
|
|
val startLine = TextWindow.getStartLineWithCursorCentered
|
|
|
|
|
(buffer, cursorIdx, origLine, windowWidth, windowHeight div 2)
|
|
|
|
|
|
|
|
|
|
val buffer = LineGap.goToLine (startLine, buffer)
|
|
|
|
|
val lineIdx = TextBuilder.getLineAbsIdx (startLine, buffer)
|
|
|
|
|
|
|
|
|
|
val drawMsg = TextBuilder.build
|
|
|
|
|
( startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, buffer
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, searchList
|
|
|
|
|
, searchString
|
|
|
|
|
, []
|
|
|
|
|
)
|
|
|
|
|
in
|
2025-09-11 23:43:09 +01:00
|
|
|
let
|
|
|
|
|
val _ = raise Fail "centering to line is unimplemented\n"
|
|
|
|
|
in
|
|
|
|
|
NormalModeWith.bufferAndCursorIdx
|
|
|
|
|
( app
|
|
|
|
|
, buffer
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, NORMAL_MODE ""
|
|
|
|
|
, startLine
|
|
|
|
|
, searchList
|
|
|
|
|
, drawMsg
|
|
|
|
|
, bufferModifyTime
|
|
|
|
|
, #visualScrollColumn app
|
|
|
|
|
)
|
|
|
|
|
end
|
2025-08-07 17:41:10 +01:00
|
|
|
end
|
2025-01-09 22:30:51 +00:00
|
|
|
end
|