pothi.love/0017-on.mouse_release

on.mouse_release = function(x,y, mouse_button)
	if Animating then return end
	if Manifest_navigator.show then
		reset_manifest_navigator()
	end
	if Pan then
		Pan = nil
		A()
	elseif Move then
		Move = nil
		A()
	elseif Cursor_node then
		Cursor_node.show_cursor = true
		edit.mouse_release(Cursor_node.editor, x,y, mouse_button)
	end
end
recompute entire layout on mouse release Recent changes have made the driver much more responsive, but it's also resulted in _never_ ever updating the box model. One quick hack to provide some control here: panning the surface (or moving a definition) updates everything. And to remain snappy it only does so on mouse release. I still need to polish when we recompute. Arguably we need to decompose A into a few different concerns and create variants that perform subsets of A's concerns. But this hacky commit helps. 2023-01-13 16:22:41 +00:00			`on.mouse_release = function(x,y, mouse_button)`
			`if Animating then return end`
bugfix: hide manifest nav after any mouse click Either we clicked on a button or we clicked somewhere else. 2023-09-10 05:52:50 +01:00			`if Manifest_navigator.show then`
			`reset_manifest_navigator()`
			`end`
recompute entire layout on mouse release Recent changes have made the driver much more responsive, but it's also resulted in _never_ ever updating the box model. One quick hack to provide some control here: panning the surface (or moving a definition) updates everything. And to remain snappy it only does so on mouse release. I still need to polish when we recompute. Arguably we need to decompose A into a few different concerns and create variants that perform subsets of A's concerns. But this hacky commit helps. 2023-01-13 16:22:41 +00:00			`if Pan then`
			`Pan = nil`
			`A()`
			`elseif Move then`
			`Move = nil`
			`A()`
			`elseif Cursor_node then`
			`Cursor_node.show_cursor = true`
			`edit.mouse_release(Cursor_node.editor, x,y, mouse_button)`
			`end`
bugfix: hide manifest nav after any mouse click Either we clicked on a button or we clicked somewhere else. 2023-09-10 05:52:50 +01:00			`end`