more reactive update, like Output panel;
authorwenzelm
Mon, 21 Sep 2015 17:59:21 +0200
changeset 61217 566f256f59bb
parent 61216 4ca490f09ec6
child 61218 04c769fe1cb5
more reactive update, like Output panel;
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()
   }
 }