2024-10-08 08:53:43 +01:00
|
|
|
structure AppWith =
|
|
|
|
|
struct
|
|
|
|
|
open AppType
|
|
|
|
|
|
2024-11-25 04:37:47 +00:00
|
|
|
fun bufferAndSize
|
2025-08-20 12:51:31 +01:00
|
|
|
( app: app_type
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newWidth
|
|
|
|
|
, newHeight
|
|
|
|
|
, newSearchList
|
|
|
|
|
, newMsgs
|
|
|
|
|
, newBufferModifyTime
|
|
|
|
|
) =
|
2024-10-08 08:53:43 +01:00
|
|
|
let
|
2024-10-26 04:46:05 +01:00
|
|
|
val
|
|
|
|
|
{ mode
|
|
|
|
|
, buffer = _
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime = _
|
2024-10-26 04:46:05 +01:00
|
|
|
, windowWidth = _
|
|
|
|
|
, windowHeight = _
|
2024-11-25 04:37:47 +00:00
|
|
|
, searchList = _
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs = _
|
2024-11-14 08:12:27 +00:00
|
|
|
, searchString
|
2024-10-26 04:46:05 +01:00
|
|
|
, startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
} = app
|
2024-10-08 08:53:43 +01:00
|
|
|
in
|
2024-10-26 04:46:05 +01:00
|
|
|
{ mode = mode
|
|
|
|
|
, buffer = newBuffer
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime = newBufferModifyTime
|
2024-10-08 08:53:43 +01:00
|
|
|
, windowWidth = newWidth
|
|
|
|
|
, windowHeight = newHeight
|
2024-11-25 04:37:47 +00:00
|
|
|
, searchList = newSearchList
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs = newMsgs
|
2024-11-14 08:12:27 +00:00
|
|
|
, searchString = searchString
|
2024-10-08 08:53:43 +01:00
|
|
|
, startLine = startLine
|
2024-10-09 10:59:32 +01:00
|
|
|
, cursorIdx = cursorIdx
|
2024-10-08 08:53:43 +01:00
|
|
|
}
|
|
|
|
|
end
|
2024-10-17 02:14:09 +01:00
|
|
|
|
2024-10-28 09:34:55 +00:00
|
|
|
fun bufferAndCursorIdx
|
2024-11-23 06:10:40 +00:00
|
|
|
( app: app_type
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newCursorIdx
|
|
|
|
|
, newMode
|
|
|
|
|
, newStartLine
|
|
|
|
|
, newSearchList
|
2024-12-17 10:40:06 +00:00
|
|
|
, newMsgs
|
2025-08-20 12:50:39 +01:00
|
|
|
, newBufferModifyTime
|
2024-11-23 06:10:40 +00:00
|
|
|
) =
|
2024-11-16 08:33:26 +00:00
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ mode = _
|
|
|
|
|
, buffer = _
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime = _
|
2024-11-16 08:33:26 +00:00
|
|
|
, cursorIdx = _
|
|
|
|
|
, startLine = _
|
|
|
|
|
, searchList = _
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs = _
|
2024-11-16 08:33:26 +00:00
|
|
|
, searchString
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
} = app
|
|
|
|
|
in
|
|
|
|
|
{ mode = newMode
|
|
|
|
|
, buffer = newBuffer
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime = newBufferModifyTime
|
2024-11-16 08:33:26 +00:00
|
|
|
, cursorIdx = newCursorIdx
|
|
|
|
|
, startLine = newStartLine
|
|
|
|
|
, searchList = newSearchList
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs = newMsgs
|
2024-11-16 08:33:26 +00:00
|
|
|
, searchString = searchString
|
|
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
}
|
|
|
|
|
end
|
|
|
|
|
|
2024-12-17 10:40:06 +00:00
|
|
|
fun mode (app: app_type, newMode, newMsgs) =
|
2024-10-26 06:01:48 +01:00
|
|
|
let
|
2024-11-14 08:12:27 +00:00
|
|
|
val
|
|
|
|
|
{ mode = _
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs = _
|
2024-11-14 08:12:27 +00:00
|
|
|
, buffer
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime
|
2024-11-14 08:12:27 +00:00
|
|
|
, searchList
|
|
|
|
|
, searchString
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, startLine
|
|
|
|
|
} = app
|
2024-10-26 06:01:48 +01:00
|
|
|
in
|
|
|
|
|
{ mode = newMode
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs = newMsgs
|
2024-10-26 06:01:48 +01:00
|
|
|
, buffer = buffer
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime = bufferModifyTime
|
2024-11-14 08:12:27 +00:00
|
|
|
, searchList = searchList
|
|
|
|
|
, searchString = searchString
|
2024-10-26 06:01:48 +01:00
|
|
|
, cursorIdx = cursorIdx
|
|
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
, startLine = startLine
|
|
|
|
|
}
|
|
|
|
|
end
|
2024-11-15 05:37:53 +00:00
|
|
|
|
2025-08-20 12:51:31 +01:00
|
|
|
fun searchList
|
|
|
|
|
( app: app_type
|
|
|
|
|
, newSearchList
|
|
|
|
|
, newBuffer
|
|
|
|
|
, newSearchString
|
|
|
|
|
, newBufferModifyTime
|
|
|
|
|
) =
|
2024-11-15 05:37:53 +00:00
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ searchList = _
|
|
|
|
|
, buffer = _
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime
|
2024-11-15 05:40:57 +00:00
|
|
|
, searchString = _
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs
|
2024-11-15 05:37:53 +00:00
|
|
|
, mode
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, startLine
|
|
|
|
|
} = app
|
|
|
|
|
in
|
|
|
|
|
{ searchList = newSearchList
|
|
|
|
|
, buffer = newBuffer
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime = newBufferModifyTime
|
2024-11-15 05:40:57 +00:00
|
|
|
, searchString = newSearchString
|
2024-12-17 10:40:06 +00:00
|
|
|
, msgs = msgs
|
2024-11-15 05:37:53 +00:00
|
|
|
, mode = mode
|
|
|
|
|
, cursorIdx = cursorIdx
|
|
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
, startLine = startLine
|
|
|
|
|
}
|
|
|
|
|
end
|
2025-03-23 07:47:38 +00:00
|
|
|
|
2025-08-20 13:50:57 +01:00
|
|
|
(* this function exists only for testing *)
|
2025-03-23 07:47:38 +00:00
|
|
|
fun idx (app, newIdx) =
|
|
|
|
|
let
|
|
|
|
|
val
|
|
|
|
|
{ startLine
|
|
|
|
|
, buffer
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime
|
2025-03-23 07:47:38 +00:00
|
|
|
, searchList
|
|
|
|
|
, searchString
|
|
|
|
|
, mode
|
|
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, msgs
|
|
|
|
|
, cursorIdx = _
|
|
|
|
|
} = app
|
|
|
|
|
in
|
|
|
|
|
{ startLine = startLine
|
|
|
|
|
, buffer = buffer
|
2025-08-20 12:50:39 +01:00
|
|
|
, bufferModifyTime = bufferModifyTime
|
2025-03-23 07:47:38 +00:00
|
|
|
, searchList = searchList
|
|
|
|
|
, searchString = searchString
|
|
|
|
|
, mode = mode
|
|
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
, msgs = msgs
|
|
|
|
|
, cursorIdx = newIdx
|
|
|
|
|
}
|
|
|
|
|
end
|
2024-10-08 08:53:43 +01:00
|
|
|
end
|