src/Tools/jEdit/src/query_dockable.scala
2016-09-05 wenzelm 2016-09-05 clarified modules;
2015-08-07 wenzelm 2015-08-07 maintain history more often;
2015-07-17 wenzelm 2015-07-17 more uniform ComponentAdapter;
2015-01-18 wenzelm 2015-01-18 tuned;
2015-01-05 wenzelm 2015-01-05 GUI.imitate_font: more explicit result size, e.g. relevant for caching; some graphview font options: Helvetica family is important for self-contained PDF; tuned;
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-07-22 wenzelm 2014-07-22 support multiple selected print operations instead of slightly odd "menu";
2014-05-21 wenzelm 2014-05-21 more uniform Font_Info.Zoom_Box; misc tuning and clarification;
2014-05-21 wenzelm 2014-05-21 tuned signature;
2014-05-19 wenzelm 2014-05-19 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus;
2014-05-08 wenzelm 2014-05-08 clarified detach_operation: ignore empty output;
2014-05-08 wenzelm 2014-05-08 tuned GUI;
2014-05-08 wenzelm 2014-05-08 tuned GUI;
2014-05-08 wenzelm 2014-05-08 tuned GUI;
2014-05-08 wenzelm 2014-05-08 enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
2014-05-08 wenzelm 2014-05-08 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
2014-05-06 wenzelm 2014-05-06 tuned GUI layout;
2014-05-06 wenzelm 2014-05-06 common support for search field, which is actually a light-weight Highlighter;
2014-05-06 wenzelm 2014-05-06 clarified GUI focus;
2014-05-06 wenzelm 2014-05-06 more uniform detach button;
2014-05-06 wenzelm 2014-05-06 renamed "Find" to "Query", with more general operations;