2023-11-21 06:23:09 +00:00
|
|
|
output_editor_state = function(editor_state)
|
|
|
|
local result = edit.initialize_state(
|
|
|
|
editor_state.bottom+5+10+5, -- top
|
|
|
|
nil, -- buttom
|
|
|
|
editor_state.left, editor_state.right,
|
2023-11-21 20:11:26 +00:00
|
|
|
Font_height, Line_height)
|
2023-11-21 06:23:09 +00:00
|
|
|
Text.redraw_all(result)
|
|
|
|
return result
|
|
|
|
end
|