2014-04-26 wenzelm [Sat, 26 Apr 2014 22:51:21 +0200] rev 56761
NEWS;
NEWS

2014-04-26 wenzelm [Sat, 26 Apr 2014 22:43:22 +0200] rev 56760
tuned message;
src/Pure/Tools/find_consts.ML

2014-04-26 wenzelm [Sat, 26 Apr 2014 22:35:19 +0200] rev 56759
proper handling of shared zoom component: update layout dynamically;
src/Tools/jEdit/src/find_dockable.scala

2014-04-26 wenzelm [Sat, 26 Apr 2014 21:49:31 +0200] rev 56758
PIDE support for find_consts;
src/Pure/Tools/find_consts.ML src/Tools/jEdit/src/find_dockable.scala

2014-04-26 wenzelm [Sat, 26 Apr 2014 21:16:50 +0200] rev 56757
some rearrangements to support multiple find operations;
src/Tools/jEdit/src/find_dockable.scala

2014-04-26 wenzelm [Sat, 26 Apr 2014 18:06:21 +0200] rev 56756
tuned;
src/Tools/jEdit/src/symbols_dockable.scala

2014-04-26 wenzelm [Sat, 26 Apr 2014 17:53:03 +0200] rev 56755
clarified GUI focus;
src/Tools/jEdit/src/symbols_dockable.scala

2014-04-26 wenzelm [Sat, 26 Apr 2014 17:25:02 +0200] rev 56754
actually observe search limit;
src/Tools/jEdit/src/symbols_dockable.scala

2014-04-26 wenzelm [Sat, 26 Apr 2014 17:20:37 +0200] rev 56753
misc tuning;
src/Tools/jEdit/src/symbols_dockable.scala

2014-04-26 wenzelm [Sat, 26 Apr 2014 15:33:13 +0200] rev 56752
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
src/Pure/GUI/gui.scala src/Tools/jEdit/src/jedit_options.scala