2023-11-15 15:04:34 +00:00
|
|
|
draw_output_border = function()
|
2023-11-26 18:33:22 +00:00
|
|
|
App.color{r=0.5, g=0.5, b=0.5}
|
2023-11-15 15:04:34 +00:00
|
|
|
-- hack: computing based on editor before output exists
|
2023-11-19 21:15:06 +00:00
|
|
|
local x1 = Current_pane.editor_state.left-5-Line_number_padding
|
|
|
|
|
local x2 = Current_pane.editor_state.right+5
|
|
|
|
|
local y1 = Current_pane.editor_state.bottom+5+10
|
2023-11-15 15:04:34 +00:00
|
|
|
-- upper border
|
|
|
|
|
love.graphics.line(x1,y1, x2,y1)
|
|
|
|
|
love.graphics.line(x1,y1, x1,y1+10)
|
|
|
|
|
love.graphics.line(x2,y1, x2,y1+10)
|
|
|
|
|
end
|