BTW, is it possible to detect double-clicks?
Not currently -- we could add this to the GUI neutral event handling
mechanism. Probably the easiest way would be to do this at the level
of backend_bases, and check for double clicks ourselves, rather than
trying to wrap double click events for all 5 GUIs.