2024-10-08 08:53:43 +01:00
|
|
|
structure AppWith =
|
|
|
|
|
struct
|
|
|
|
|
open AppType
|
|
|
|
|
|
|
|
|
|
fun bufferAndSize (app: app_type, newBuffer, newWidth, newHeight) =
|
|
|
|
|
let
|
2024-10-18 06:44:45 +01:00
|
|
|
val
|
|
|
|
|
{ buffer = _
|
|
|
|
|
, windowWidth = _
|
|
|
|
|
, windowHeight = _
|
|
|
|
|
, startLine
|
|
|
|
|
, cursorIdx
|
|
|
|
|
, preferredColumn
|
|
|
|
|
} = app
|
2024-10-08 08:53:43 +01:00
|
|
|
in
|
|
|
|
|
{ buffer = newBuffer
|
|
|
|
|
, windowWidth = newWidth
|
|
|
|
|
, windowHeight = newHeight
|
|
|
|
|
, startLine = startLine
|
2024-10-09 10:59:32 +01:00
|
|
|
, cursorIdx = cursorIdx
|
2024-10-18 06:44:45 +01:00
|
|
|
, preferredColumn = preferredColumn
|
2024-10-08 08:53:43 +01:00
|
|
|
}
|
|
|
|
|
end
|
2024-10-17 02:14:09 +01:00
|
|
|
|
2024-10-19 07:03:32 +01:00
|
|
|
fun bufferAndCursorIdx (app: app_type, newBuffer, newCursorIdx, newColumn) =
|
2024-10-17 02:14:09 +01:00
|
|
|
let
|
2024-10-18 06:44:45 +01:00
|
|
|
val
|
|
|
|
|
{ buffer = _
|
|
|
|
|
, cursorIdx = _
|
2024-10-19 07:03:32 +01:00
|
|
|
, preferredColumn = _
|
2024-10-18 06:44:45 +01:00
|
|
|
, windowWidth
|
|
|
|
|
, windowHeight
|
|
|
|
|
, startLine
|
|
|
|
|
} = app
|
2024-10-17 02:14:09 +01:00
|
|
|
in
|
|
|
|
|
{ buffer = newBuffer
|
|
|
|
|
, cursorIdx = newCursorIdx
|
2024-10-19 07:03:32 +01:00
|
|
|
, preferredColumn = newColumn
|
2024-10-17 02:14:09 +01:00
|
|
|
, windowWidth = windowWidth
|
|
|
|
|
, windowHeight = windowHeight
|
|
|
|
|
, startLine = startLine
|
|
|
|
|
}
|
|
|
|
|
end
|
2024-10-08 08:53:43 +01:00
|
|
|
end
|