2022-12-24 05:35:57 +00:00
|
|
|
box_height = function(node)
|
2023-10-25 15:45:09 +01:00
|
|
|
-- return the height of a text editor node (explicit width). The result is unscaled.
|
|
|
|
local y = 0
|
2023-04-23 06:29:22 +01:00
|
|
|
for i=1,#node.editor.lines do
|
|
|
|
local line = node.editor.lines[i]
|
|
|
|
if node.editor.line_cache[i] == nil then
|
|
|
|
node.editor.line_cache[i] = {}
|
|
|
|
end
|
2023-10-25 15:45:09 +01:00
|
|
|
node.editor.line_cache[i].fragments = nil
|
2023-04-23 06:29:22 +01:00
|
|
|
node.editor.line_cache[i].screen_line_starting_pos = nil
|
|
|
|
Text.populate_screen_line_starting_pos(node.editor, i)
|
2023-10-25 15:45:09 +01:00
|
|
|
y = y + node.editor.line_height*#node.editor.line_cache[i].screen_line_starting_pos
|
2023-04-23 06:29:22 +01:00
|
|
|
Text.clear_screen_line_cache(node.editor, i)
|
|
|
|
end
|
2023-10-25 17:23:05 +01:00
|
|
|
return y/Viewport.zoom
|
2023-04-03 01:05:54 +01:00
|
|
|
end
|