update GUI components after init;
authorwenzelm
Tue, 29 May 2012 23:19:37 +0200
changeset 48026 8559d681a617
parent 48025 0f1d95663dff
child 48027 69ba790960ba
update GUI components after init;
src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue May 29 22:44:02 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue May 29 23:19:37 2012 +0200
@@ -133,6 +133,7 @@
     Isabelle.session.global_settings += main_actor
     Isabelle.session.commands_changed += main_actor
     Isabelle.session.caret_focus += main_actor
+    handle_update()
   }
 
   override def exit()
@@ -178,6 +179,4 @@
 
   private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
   add(controls.peer, BorderLayout.NORTH)
-
-  handle_update()
 }