more aggressive update -- potentially relevant for previously is_outdated output;

--- 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)