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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
