[isabelle-dev] NEWS: Improved management of dockable windows

[Makarius]

On Wed, 21 May 2014, Lars Noschinski wrote:

>  * At least for the output window, I'd like to see a more direct to
>    to detach a window than the context menu.

I was thinking of that, when making that change, but did not find a 
solution yet.  The general idea is that there are some common operations 
like "zoom" or "detach" for these movable windows (or tooltips).

It remains to be seen how to turn this into an "action" of jEdit, and then 
to find a free key.  X11 users could actually remap capslock and bind it 
to that action :-) Maybe there are some more portable mechanisms that 
could be applied eventually.


 	Makarius