# HG changeset patch
# User wenzelm
# Date 1442851161 -7200
# Node ID 566f256f59bbf9d528ffa3388e270c9254605917
# Parent  4ca490f09ec6ec85cf63dfcdfc23c828d3d0a34f
more reactive update, like Output panel;

diff -r 4ca490f09ec6 -r 566f256f59bb src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Mon Sep 21 17:42:31 2015 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Sep 21 17:59:21 2015 +0200
@@ -111,6 +111,9 @@
       case _: Session.Global_Options =>
         GUI_Thread.later { handle_resize() }
 
+      case changed: Session.Commands_Changed =>
+        if (changed.assignment) GUI_Thread.later { maybe_update() }
+
       case Session.Caret_Focus =>
         GUI_Thread.later { maybe_update() }
     }
@@ -118,9 +121,11 @@
   override def init()
   {
     PIDE.session.global_options += main
+    PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
     handle_resize()
     print_state.activate()
+    maybe_update()
   }
 
   override def exit()
@@ -128,6 +133,7 @@
     print_state.deactivate()
     PIDE.session.caret_focus -= main
     PIDE.session.global_options -= main
+    PIDE.session.commands_changed -= main
     delay_resize.revoke()
   }
 }