|
code_editor_state = function()
|
|
local result = edit.initialize_state(
|
|
Menu_bottom + 20, -- top
|
|
code_editor_bottom_margin(),
|
|
Menu_left + 50 + Line_number_padding, -- left
|
|
editor_right_margin(),
|
|
Font, Font_height, Line_height)
|
|
Text.redraw_all(result)
|
|
return result
|
|
end |