# HG changeset patch
# User wenzelm
# Date 1357658722 -3600
# Node ID 205d12333fdc7035db3516b71197776ca11b33b6
# Parent  6973b3f413340eb4952bd5c1e09ce0991f2b75c5
more aggressive update -- potentially relevant for previously is_outdated output;

diff -r 6973b3f41334 -r 205d12333fdc src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Jan 08 16:23:07 2013 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Jan 08 16:25:22 2013 +0100
@@ -93,7 +93,8 @@
         case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
         case changed: Session.Commands_Changed =>
-          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
+          val restriction = if (changed.assignment) None else Some(changed.commands)
+          Swing_Thread.later { handle_update(do_update, restriction) }
         case Session.Caret_Focus =>
           Swing_Thread.later { handle_update(do_update, None) }
         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)