2025-08-31 07:40:31 +01:00
|
|
|
structure NormalSearchModeWith =
|
|
|
|
|
struct
|
|
|
|
|
open AppType
|
|
|
|
|
|
|
|
|
|
fun returnToNormalMode
|
|
|
|
|
( app: app_type
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newSearchList
|
|
|
|
|
, newStartLine
|
|
|
|
|
, newMode
|
2025-10-08 05:02:15 +01:00
|
|
|
, newDfa
|
2025-08-31 07:40:31 +01:00
|
|
|
, newMsgs
|
|
|
|
|
) =
|
|
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ mode = _
|
|
|
|
|
, buffer = _
|
|
|
|
|
, searchList = _
|
|
|
|
|
, startLine = _
|
|
|
|
|
, msgs = _
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa = _
|
2025-08-31 07:40:31 +01:00
|
|
|
, bufferModifyTime
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn
|
2025-08-31 07:40:31 +01:00
|
|
|
} = app
|
|
|
|
|
in
|
|
|
|
|
{ mode = newMode
|
|
|
|
|
, buffer = newBuffer
|
|
|
|
|
, searchList = newSearchList
|
|
|
|
|
, startLine = newStartLine
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa = newDfa
|
2025-08-31 07:40:31 +01:00
|
|
|
, bufferModifyTime = bufferModifyTime
|
|
|
|
|
, msgs = newMsgs
|
|
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
, cursorIdx = cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn = visualScrollColumn
|
2025-08-31 07:40:31 +01:00
|
|
|
}
|
|
|
|
|
end
|
2025-09-01 02:18:23 +01:00
|
|
|
|
|
|
|
|
fun changeTempSearchString
|
|
|
|
|
(app: app_type, newBuffer, newStartLine, newMode, newMsgs) =
|
|
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ mode = _
|
|
|
|
|
, buffer = _
|
|
|
|
|
, searchList
|
|
|
|
|
, startLine = _
|
|
|
|
|
, msgs = _
|
|
|
|
|
, bufferModifyTime
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa
|
2025-09-01 02:18:23 +01:00
|
|
|
} = app
|
|
|
|
|
in
|
|
|
|
|
{ mode = newMode
|
|
|
|
|
, buffer = newBuffer
|
|
|
|
|
, startLine = newStartLine
|
|
|
|
|
, msgs = newMsgs
|
|
|
|
|
, searchList = searchList
|
|
|
|
|
, bufferModifyTime = bufferModifyTime
|
|
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
, cursorIdx = cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn = visualScrollColumn
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa = dfa
|
2025-09-01 02:18:23 +01:00
|
|
|
}
|
|
|
|
|
end
|
2025-09-01 12:52:26 +01:00
|
|
|
|
|
|
|
|
fun searchList (app: app_type, newSearchList) =
|
|
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ mode
|
|
|
|
|
, buffer
|
|
|
|
|
, searchList = _
|
|
|
|
|
, startLine
|
|
|
|
|
, msgs
|
|
|
|
|
, bufferModifyTime
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa
|
2025-09-01 12:52:26 +01:00
|
|
|
} = app
|
|
|
|
|
in
|
|
|
|
|
{ mode = mode
|
|
|
|
|
, searchList = newSearchList
|
|
|
|
|
, buffer = buffer
|
|
|
|
|
, startLine = startLine
|
|
|
|
|
, msgs = msgs
|
|
|
|
|
, bufferModifyTime = bufferModifyTime
|
|
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
, cursorIdx = cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn = visualScrollColumn
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa = dfa
|
2025-09-01 12:52:26 +01:00
|
|
|
}
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun bufferAndSize
|
2025-09-14 10:28:42 +01:00
|
|
|
( app: app_type
|
|
|
|
|
, newMode
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newWindowWidth
|
|
|
|
|
, newWindowHeight
|
|
|
|
|
, newMsgs
|
|
|
|
|
) =
|
2025-09-01 12:52:26 +01:00
|
|
|
let
|
|
|
|
|
val
|
2025-09-14 10:28:42 +01:00
|
|
|
{ mode = _
|
2025-09-01 12:52:26 +01:00
|
|
|
, windowWidth = _
|
|
|
|
|
, windowHeight = _
|
|
|
|
|
, msgs = _
|
|
|
|
|
, buffer = _
|
|
|
|
|
, searchList
|
|
|
|
|
, startLine
|
|
|
|
|
, bufferModifyTime
|
|
|
|
|
, cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa
|
2025-09-01 12:52:26 +01:00
|
|
|
} = app
|
|
|
|
|
in
|
2025-09-14 10:28:42 +01:00
|
|
|
{ mode = newMode
|
2025-09-01 12:52:26 +01:00
|
|
|
, buffer = newBuffer
|
|
|
|
|
, windowWidth = newWindowWidth
|
|
|
|
|
, windowHeight = newWindowHeight
|
|
|
|
|
, msgs = newMsgs
|
|
|
|
|
, searchList = searchList
|
|
|
|
|
, startLine = startLine
|
|
|
|
|
, bufferModifyTime = bufferModifyTime
|
|
|
|
|
, cursorIdx = cursorIdx
|
2025-09-11 15:26:30 +01:00
|
|
|
, visualScrollColumn = visualScrollColumn
|
2025-10-08 05:02:15 +01:00
|
|
|
, dfa = dfa
|
2025-09-01 12:52:26 +01:00
|
|
|
}
|
|
|
|
|
end
|
2025-08-31 07:40:31 +01:00
|
|
|
end
|