recovered handle_resize from 5922db0430f1;

--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Feb 01 19:57:58 2016 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Feb 04 12:11:27 2016 +0100
@@ -129,6 +129,7 @@
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later {
+          handle_resize()
           output_state_button.selected = output_state
           handle_update(do_update, None)
         }